initial version of 'isar proof assistant (Isabelle/Isar);

1 files changed, 41 insertions, 0 deletions

diff --git a/isar/ProofGeneral.ML b/isar/ProofGeneral.ML
new file mode 100644
index 00000000..8cf11f2f
--- /dev/null
+++ b/isar/ProofGeneral.ML
@@ -0,0 +1,41 @@
+(* 
+   Isabelle/Isar configuration for Proof General.
+
+   Author:  David Aspinall <da@dcs.ed.ac.uk>
+   Contact: Isabelle maintainer <isabelle@dcs.ed.ac.uk>
+
+   ProofGeneral.ML,v 2.16 1998/11/03 16:29:30 da Exp
+
+MMW: I have temporarily removed the theory loader patches, since it
+kept crashing on me.
+*)
+
+
+(** configure output channels to decorate output **)
+
+(*messages*)
+writeln_fn :=
+  (std_output o suffix "\n" o enclose (oct_char "360") (oct_char "361"));
+warning_fn :=
+  (std_output o suffix "\n" o enclose (oct_char "362") (oct_char "363") o prefix_lines "### ");
+error_fn :=
+  (std_output o suffix "\n" o enclose (oct_char "364") (oct_char "365") o prefix_lines "*** ");
+
+(*prompts*)
+Source.decorate_prompt_fn := (fn s => s ^ oct_char "372");
+
+(*theory / proof state*)
+current_goals_markers :=
+  let
+    val begin_state = oct_char "366";
+    val end_state= oct_char "367";
+    val begin_goal = oct_char "370";
+  in (begin_state, end_state, begin_goal) end;
+
+Toplevel.print_state_fn :=
+  (Library.setmp writeln_fn (std_output o suffix "\n") Toplevel.print_state_default);
+
+
+print_mode := ["ProofGeneral"];
+
+Isar.main();