src/Pure/Interface/proof_general.ML
changeset 6699 1471f2bd74a0
child 6720 353bd9b74b1f
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Interface/proof_general.ML	Fri May 21 16:26:06 1999 +0200
     1.3 @@ -0,0 +1,93 @@
     1.4 +(*  Title:      Pure/Interface/proof_general.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Markus Wenzel, TU Muenchen
     1.7 +
     1.8 +Configuration for ProofGeneral of LFCS Edinburgh.
     1.9 +*)
    1.10 +
    1.11 +signature PROOF_GENERAL =
    1.12 +sig
    1.13 +  val setup: (theory -> theory) list
    1.14 +  val init: bool -> unit
    1.15 +end;
    1.16 +
    1.17 +structure ProofGeneral: PROOF_GENERAL =
    1.18 +struct
    1.19 +
    1.20 +
    1.21 +(** compile-time theory setup **)
    1.22 +
    1.23 +(* token translations *)
    1.24 +
    1.25 +val proof_generalN = "ProofGeneral";
    1.26 +
    1.27 +local
    1.28 +
    1.29 +val end_tag = oct_char "350";
    1.30 +val tclass_tag = oct_char "351";
    1.31 +val tfree_tag = oct_char "352";
    1.32 +val tvar_tag = oct_char "353";
    1.33 +val free_tag = oct_char "354";
    1.34 +val bound_tag = oct_char "355";
    1.35 +val var_tag = oct_char "356";
    1.36 +
    1.37 +fun tagit p x = (p ^ x ^ end_tag, real (size x));
    1.38 +
    1.39 +in
    1.40 +
    1.41 +val proof_general_trans =
    1.42 + Syntax.tokentrans_mode proof_generalN
    1.43 +  [("class", tagit tclass_tag),
    1.44 +   ("tfree", tagit tfree_tag),
    1.45 +   ("tvar", tagit tvar_tag),
    1.46 +   ("free", tagit free_tag),
    1.47 +   ("bound", tagit bound_tag),
    1.48 +   ("var", tagit var_tag)];
    1.49 +
    1.50 +end;
    1.51 +
    1.52 +
    1.53 +(* setup *)
    1.54 +
    1.55 +val setup = [Theory.add_tokentrfuns proof_general_trans];
    1.56 +
    1.57 +
    1.58 +
    1.59 +(** run-time initialization **)
    1.60 +
    1.61 +(* messages *)
    1.62 +
    1.63 +fun decorate_lines bg en "" = std_output o suffix "\n" o enclose bg en
    1.64 +  | decorate_lines bg en prfx = std_output o suffix "\n" o enclose bg en o prefix_lines prfx;
    1.65 +
    1.66 +fun setup_messages () =
    1.67 + (writeln_fn := (decorate_lines (oct_char "360") (oct_char "361") "");
    1.68 +  warning_fn := (decorate_lines (oct_char "362") (oct_char "363") "### ");
    1.69 +  error_fn := (decorate_lines (oct_char "364") (oct_char "365") "*** "));
    1.70 +
    1.71 +
    1.72 +(* theory / proof state *)
    1.73 +
    1.74 +fun setup_state () =
    1.75 +  (current_goals_markers :=
    1.76 +    let
    1.77 +      val begin_state = oct_char "366";
    1.78 +      val end_state= oct_char "367";
    1.79 +      val begin_goal = oct_char "370";
    1.80 +    in (begin_state, end_state, begin_goal) end;
    1.81 +  Toplevel.print_state_fn :=
    1.82 +    (Library.setmp writeln_fn (std_output o suffix "\n") Toplevel.print_state_default);
    1.83 +  Toplevel.prompt_state_fn := (suffix (oct_char "372") o Toplevel.prompt_state_default));
    1.84 +
    1.85 +
    1.86 +(* init *)
    1.87 +
    1.88 +fun init isar =
    1.89 + (setup_messages ();
    1.90 +  setup_state ();
    1.91 +  print_mode := [proof_generalN];
    1.92 +  set quick_and_dirty;
    1.93 +  if isar then Isar.main () else ());
    1.94 +
    1.95 +
    1.96 +end;