src/Pure/Interface/proof_general.ML
author wenzelm
Fri Aug 06 22:43:51 1999 +0200 (1999-08-06 ago)
changeset 7195 a38dc0c6b244
parent 7193 cc7a89d233f7
child 7210 ae9a645e8728
permissions -rw-r--r--
made SML happy;
     1 (*  Title:      Pure/Interface/proof_general.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 Configuration for ProofGeneral of LFCS Edinburgh.
     6 *)
     7 
     8 signature PROOF_GENERAL =
     9 sig
    10   val write_keywords: unit -> unit
    11   val setup: (theory -> theory) list
    12   val help: unit -> unit
    13   val show_context: unit -> theory
    14   val kill_goal: unit -> unit
    15   val repeat_undo: int -> unit
    16   val init: bool -> unit
    17   val isa_restart: unit -> unit
    18 end;
    19 
    20 structure ProofGeneral: PROOF_GENERAL =
    21 struct
    22 
    23 
    24 (** generate keyword classification file **)
    25 
    26 local
    27 
    28 val regexp_meta = explode ".*+?[]^$";
    29 val regexp_quote = implode o map (fn c => if c mem regexp_meta then "\\\\" ^ c else c) o explode;
    30 
    31 fun defconst name strs =
    32   "\n(defconst isar-keywords-" ^ name ^
    33   "\n  '(" ^ space_implode "\n    " (map (quote o regexp_quote) strs) ^ "))\n";
    34 
    35 fun make_elisp_commands commands kind =
    36   defconst kind (mapfilter (fn (c, _, k, _) => if k = kind then Some c else None) commands);
    37 
    38 fun make_elisp_syntax (keywords, commands) =
    39   ";;\n\
    40   \;; Keyword classification tables for Isabelle/Isar.\n\
    41   \;; This file generated by Isabelle -- DO NOT EDIT!\n\
    42   \;;\n\
    43   \;; $" ^ "Id$\n\
    44   \;;\n" ^
    45   defconst "minor" (filter Syntax.is_identifier keywords) ^
    46   implode (map (make_elisp_commands commands) OuterSyntax.Keyword.kinds) ^
    47   "\n(provide 'isar-keywords)\n";
    48 
    49 val keywords_file = "isar-keywords.el";
    50 
    51 in
    52 
    53 fun write_keywords () =
    54   File.write (Path.unpack keywords_file)
    55     (make_elisp_syntax (OuterSyntax.dest_keywords (), OuterSyntax.dest_parsers ()));
    56 
    57 end;
    58 
    59 
    60 
    61 (** compile-time theory setup **)
    62 
    63 (* token translations *)
    64 
    65 val proof_generalN = "ProofGeneral";
    66 
    67 local
    68 
    69 val end_tag = oct_char "350";
    70 val tclass_tag = oct_char "351";
    71 val tfree_tag = oct_char "352";
    72 val tvar_tag = oct_char "353";
    73 val free_tag = oct_char "354";
    74 val bound_tag = oct_char "355";
    75 val var_tag = oct_char "356";
    76 
    77 fun tagit p x = (p ^ x ^ end_tag, real (size x));
    78 
    79 in
    80 
    81 val proof_general_trans =
    82  Syntax.tokentrans_mode proof_generalN
    83   [("class", tagit tclass_tag),
    84    ("tfree", tagit tfree_tag),
    85    ("tvar", tagit tvar_tag),
    86    ("free", tagit free_tag),
    87    ("bound", tagit bound_tag),
    88    ("var", tagit var_tag)];
    89 
    90 end;
    91 
    92 
    93 (* setup *)
    94 
    95 val setup = [Theory.add_tokentrfuns proof_general_trans];
    96 
    97 
    98 
    99 (** run-time operations **)
   100 
   101 (* messages *)
   102 
   103 val plain_output = std_output o suffix "\n";
   104 fun plain_writeln x = Library.setmp writeln_fn plain_output x;
   105 
   106 fun decorate_lines bg en "" = plain_output o enclose bg en
   107   | decorate_lines bg en prfx = plain_output o enclose bg en o prefix_lines prfx;
   108 
   109 fun setup_messages () =
   110  (writeln_fn := (decorate_lines (oct_char "360") (oct_char "361") "");
   111   warning_fn := (decorate_lines (oct_char "362") (oct_char "363") "### ");
   112   error_fn := (decorate_lines (oct_char "364") (oct_char "365") "*** "));
   113 
   114 
   115 (* theory / proof state *)
   116 
   117 fun print_current_goals n max th = plain_writeln (Goals.print_current_goals_default n max) th;
   118 
   119 fun setup_state isar =
   120   (current_goals_markers :=
   121     let
   122       val begin_state = oct_char "366";
   123       val end_state= oct_char "367";
   124       val begin_goal = oct_char "370";
   125     in (begin_state, end_state, begin_goal) end;
   126   if isar then
   127    (Toplevel.print_state_fn := plain_writeln Toplevel.print_state_default;
   128     Toplevel.prompt_state_fn := (suffix (oct_char "372") o Toplevel.prompt_state_default))
   129   else Goals.print_current_goals_fn := print_current_goals);
   130 
   131 
   132 (* theory loader actions *)
   133 
   134 local
   135 
   136 fun tell_pg msg name = writeln ("Proof General, " ^ msg ^ " " ^ quote name);
   137 
   138 fun isa_action action name =
   139   let val files = map (File.sysify_path o #1) (ThyInfo.loaded_files name) in
   140     if action = ThyInfo.Update then seq (tell_pg "this file is loaded:") files
   141     else seq (tell_pg "you can unlock the file") files
   142   end;
   143 
   144 fun isar_action action name =
   145   if action = ThyInfo.Update then tell_pg "this theory is loaded:" name
   146   else tell_pg "you can unlock the theory" name;
   147 
   148 in
   149   fun setup_thy_loader isar = ThyInfo.add_hook (if isar then isar_action else isa_action);
   150 end;
   151 
   152 
   153 (* some top-level commands for ProofGeneral/isa *)
   154 
   155 val help = writeln o Session.welcome;
   156 val show_context = Context.the_context;
   157 
   158 fun kill_goal () =
   159   (Goal "PROP no_goal_supplied"; writeln ("Proof General, please clear the goals buffer."));
   160 
   161 fun repeat_undo 0 = ()
   162   | repeat_undo n = (undo(); repeat_undo (n - 1));
   163 
   164 
   165 fun isa_restart () =
   166  (ml_prompts (">" ^ oct_char "372") ("-" ^ oct_char "373");
   167   ThyInfo.touch_all_thys ();
   168   kill_goal ();
   169   writeln ("Proof General, please clear the response buffer.");
   170   writeln "Isabelle Proof General: Isabelle process ready!");
   171 
   172 
   173 (* init *)
   174 
   175 fun init isar =
   176  (setup_messages ();
   177   setup_state isar;
   178   setup_thy_loader isar;
   179   print_mode := [proof_generalN];
   180   set quick_and_dirty;
   181   if isar then Isar.sync_main () else isa_restart ());
   182 
   183 
   184 end;