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
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
* 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
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
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
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
