Re: [isabelle-dev] misc problems
On Tue, 20 Mar 2012, Lawrence Paulson wrote: On the other hand, jedit looks beautiful. If I'm lucky, I can do a basic demo using that To make it look even better on Mac OS X, you can enable native look and feel via Utilities / Global Options / Appearance. (This needs to be done manually only for repository versions.) though I'm still not very skilled with it. I've required myself 2 full weeks to unlearn Escape-Meta-Alt-Control-Shift things to be able to use jEdit with its more standard key bindings. The time was well invested, though. What is escpecially useful is Hypersearch in the regular Find dialog, or the Firefox-style search bar. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] jEdit import theories
On Tue, 20 Mar 2012, Christian Sternagel wrote: Hi there, I am using an environment variable in an import statement like imports $VAR/Theory.thy in batch-mode this works fine. However, in jEdit I get an error message indicating Missing theory (file ...) where the path in the error message shows that $VAR was used relative to the path of the surrounding theory file. $VAR contains something like ~/some-path and was intended as being applied globally. changeset: e3a3f161ad70 jedit_build: 20120313 Odd, I think it should work. There is an explicit treatment of symbolic Isabelle paths (with a certain notion of variables) and the jEdit/JVM platform path notion. See also http://isabelle.in.tum.de/repos/isabelle/file/1ab41ea5b1c6/src/Tools/jEdit/src/jedit_thy_load.scala#l22 What does not work right now is to use VFS paths of jEdit together with Isabelle ones. I would love to see theory sources being loaded via ssh or http at some point ... In the example above, do you have a literal ~ or its expansion by the operating system shell? It is more robust to use $HOME in shell scripts if you mean home. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
