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