Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Enable new Proof General code again after SML/NJ compatibility fixes by Florian.
authoraspinall
Fri, 29 Dec 2006 16:47:49 +0100
changeset 21930 918fb0fb5c72
parent 21929 fb0cd849bc60
child 21931 314f9e2a442c
Enable new Proof General code again after SML/NJ compatibility fixes by Florian.
src/Pure/ROOT.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/ROOT.ML	Fri Dec 29 16:46:39 2006 +0100
+++ b/src/Pure/ROOT.ML	Fri Dec 29 16:47:49 2006 +0100
@@ -86,9 +86,9 @@
 (* Next line is OLD CODE: in case you have problems, uncomment next line and 
    comment out line after. Please report any problems to da@inf.ed.ac.uk.
    Plan is to remove old code very soon. *)
-(use |> setmp proofs 1 |> setmp quick_and_dirty true) "proof_general.ML"; 
-(* Next line is NEW CODE.  Currently broken on SMLNJ. *)
-(* cd "ProofGeneral"; use "ROOT.ML"; cd "..";  new code *)
+(*(use |> setmp proofs 1 |> setmp quick_and_dirty true) "proof_general.ML"; *)
+(* Next line is NEW CODE.  Hopefully now working on SMLNJ and Poly/ML. *)
+cd "ProofGeneral"; use "ROOT.ML"; cd ".."; 
 
 use_thy "Pure";
 structure Pure = struct val thy = theory "Pure" end;
isabelle