[isabelle-dev] syntax errors cause hanging

[Lawrence Paulson]

I remember when you could build a logic by typing “isabelle make", and if an error occurred somewhere, it would terminate with an error message.

I am trying to make textual changes now, and I find that “isabelle make" simply hangs. if I terminate it, I discover where I have introduced some sort of syntax error. See the attached text.

Why can't it terminate upon reaching an error, like before? It's not in a loop. PG similarly hangs and must be killed.

Larry

~/isabelle/Repos/src/ZF: isabelle makemake[2]: Nothing to be done for `Pure'.
Building ZF ...
^CZF FAILED
(see also /Users/lp15/isabelle/Repos/heaps/polyml-5.4.0_x86-darwin/log/ZF)

*** Theory loader: failed to load "Main" (unresolved "Main_ZF")
*** Theory loader: failed to load "AC" (unresolved "Main_ZF")
*** Theory loader: failed to load "Zorn" (unresolved "AC")
*** Theory loader: failed to load "Cardinal_AC" (unresolved "Zorn")
*** Theory loader: failed to load "InfDatatype" (unresolved "Cardinal_AC")
*** Theory loader: failed to load "Main_ZFC" (unresolved "Main_ZF", "InfDatatype")
*** Theory loader: undefined theory entry for "pair"
*** Theory loader: undefined theory entry for "equalities"
*** Outer syntax error (line 26 of "~~/src/ZF/Bin.thy"): command expected,
*** but symbolic identifier \<or> (line 26 of "~~/src/ZF/Bin.thy") was found
*** At command "<malformed>" (line 24 of "~~/src/ZF/Bin.thy")
*** Outer syntax error (line 14 of "~~/src/ZF/List_ZF.thy"): command expected,
*** but symbolic identifier \<or> (line 14 of "~~/src/ZF/List_ZF.thy") was found
*** At command "<malformed>" (line 13 of "~~/src/ZF/List_ZF.thy")
*** Failed to finish proof
*** At command "by" (line 80 of "~~/src/ZF/pair.thy")
*** Failed to finish proof
*** At command "by" (line 334 of "~~/src/ZF/upair.thy")
Exception- TOPLEVEL_ERROR raised
*** ML error