From 9bafbd1b551c9cf8d7c3a7fb96511966ed094831 Mon Sep 17 00:00:00 2001 From: Makarius Wenzel Date: Fri, 16 Apr 1999 16:15:27 +0000 Subject: initial version of 'isar proof assistant (Isabelle/Isar); --- isar/ProofGeneral.ML | 41 +++++++++++++++++++++++++++++++++++++++++ 1 file changed, 41 insertions(+) create mode 100644 isar/ProofGeneral.ML (limited to 'isar/ProofGeneral.ML') 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 + Contact: Isabelle maintainer + + 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(); -- cgit v1.2.3