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