Re: [isabelle-dev] Remaining uses of Proof General?
On 27.06.2014 23:47, Makarius wrote: Just a side remark: in the repository version we are talking about, and thus the coming release, ML in auxiliary files works smoothly and often better than the ML blocks, because the file gets its own ML mode. For ML files, I occasionally had the problem that hovering would not work. It usually recovered after some time. I haven't been able to pin it down to a certain situation yet. The file in question has around 400-500 lines. I /think/, this refers to d3d91422f4 (haven't worked enough with later revisions yet). It might be coincidence, but I haven't encountered this behaviour with ML blocks yet. -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] JEdit FAILED
The problem here is the missing unzip executable on the test machine. After a second look at the return code 9, I end up with the unzip man page (on lxbroy10): 9 the specified zipfiles were not found. Having a look at the code val jedit_actions = Lazy.lazy (fn () = (case Isabelle_System.bash_output unzip -p \$JEDIT_HOME/dist/jedit.jar\ org/gjt/sp/jedit/actions.xml of (txt, 0) = (case XML.parse txt of XML.Elem ((ACTIONS, _), body) = maps (parse_named ACTION) body | _ = []) | (_, rc) = error (Cannot unzip jedit.jar\nreturn code = ^ string_of_int rc))); suggests that something is bad with $JEDIT_HOME in the mira build environment. Maybe someone of the TUM guys can have a look at that. Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] NEWS: Updated and extended manuals
* Updated and extended manuals: codegen, datatypes, implementation, jedit, system. This refers to Isabelle/96f970d1522b. The list of updated manuals is based on a quick glance over the repository changes, and may be incomplete. Maybe the maintainers of manuals want to check if it makes sense. I've spent myself very pleasant weeks in the Perigord Noir, to do maybe 2000km of cycling and 40 pages of manual updates. The Isabelle/jEdit manual is now quite substantial. I've enjoyed editing it with Isabelle/jEdit itself (on a very old 2-core Mac Book Pro), using the Console/Scala shell to run the Build_Doc.build_doc jobs. Apple full-screen mode now also works nicely, if the icon in the window corner is used, not the jEdit menu entry. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] JEdit FAILED
On Sat, 28 Jun 2014, Florian Haftmann wrote: suggests that something is bad with $JEDIT_HOME in the mira build environment. JEDIT_HOME is a normal Isabelle setting, provided by the etc/settings of that component within Isabelle. So it should normally be there, although I don't understand the mira setup. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] JEdit FAILED
On Sat, 28 Jun 2014, Makarius wrote: On Sat, 28 Jun 2014, Florian Haftmann wrote: suggests that something is bad with $JEDIT_HOME in the mira build environment. JEDIT_HOME is a normal Isabelle setting, provided by the etc/settings of that component within Isabelle. So it should normally be there, although I don't understand the mira setup. Another guess: Isabelle/jEdit is really missing, because of a lacking isabelle jedit -b that is done in regular makedist (e.g. in isatest). Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Error highlighting in ML for @{lemma}
On Sat, 28 Jun 2014, Lars Noschinski wrote: If I insert a lemma antiquotation in ML code with a proposition with a type error, the error message is not attached to the proposition or the antiquotation but to the whole block or file of ML. This refers to 13b06c6261. That is a consequence of the syntax check phases still being without detailed position information. As a fall-back the position of the command transaction is used, i.e. the keyword. For 'ML' or 'text' that might be far away from the occurrence of the error in the antiquotation. Even more annoying in practice is the lack of positions for type errors in plain terms within formal specifications of the theory. I take this report as a reminder and refreshment of the priority of this non-PIDE compliant part of the system, but it won't be addressed for the coming release. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
