src/Pure/proof_general.ML
author wenzelm
Mon Jan 21 22:27:34 2002 +0100 (2002-01-21)
changeset 12833 9f3226cfe021
parent 12780 6b41c750451c
child 13273 6fea54cf6fb5
permissions -rw-r--r--
full_proofs;
wenzelm@12780
     1
(*  Title:      Pure/proof_general.ML
wenzelm@12778
     2
    ID:         $Id$
wenzelm@12778
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@12778
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
wenzelm@12778
     5
wenzelm@12778
     6
Isabelle configuration for Proof General (see http://www.proofgeneral.org).
wenzelm@12778
     7
*)
wenzelm@12778
     8
wenzelm@12778
     9
signature PROOF_GENERAL =
wenzelm@12778
    10
sig
wenzelm@12778
    11
  val setup: (theory -> theory) list
wenzelm@12778
    12
  val update_thy_only: string -> unit
wenzelm@12778
    13
  val try_update_thy_only: string -> unit
wenzelm@12778
    14
  val inform_file_processed: string -> unit
wenzelm@12778
    15
  val inform_file_retracted: string -> unit
wenzelm@12778
    16
  val thms_containing: string list -> unit
wenzelm@12778
    17
  val help: unit -> unit
wenzelm@12778
    18
  val show_context: unit -> theory
wenzelm@12778
    19
  val kill_goal: unit -> unit
wenzelm@12778
    20
  val repeat_undo: int -> unit
wenzelm@12778
    21
  val isa_restart: unit -> unit
wenzelm@12833
    22
  val full_proofs: bool -> unit
wenzelm@12778
    23
  val init: bool -> unit
wenzelm@12778
    24
  val write_keywords: string -> unit
wenzelm@12778
    25
end;
wenzelm@12778
    26
wenzelm@12778
    27
structure ProofGeneral: PROOF_GENERAL =
wenzelm@12778
    28
struct
wenzelm@12778
    29
wenzelm@12778
    30
(* print modes *)
wenzelm@12778
    31
wenzelm@12778
    32
val proof_generalN = "ProofGeneral";
wenzelm@12778
    33
val xsymbolsN = "xsymbols";
wenzelm@12778
    34
wenzelm@12778
    35
val pgmlN = "PGML";
wenzelm@12778
    36
fun pgml () = pgmlN mem_string ! print_mode;
wenzelm@12778
    37
wenzelm@12778
    38
wenzelm@12778
    39
(* text output *)
wenzelm@12778
    40
wenzelm@12778
    41
local
wenzelm@12778
    42
wenzelm@12778
    43
fun xsymbols_output s =
wenzelm@12778
    44
  if xsymbolsN mem_string ! print_mode andalso exists_string (equal "\\") s then
wenzelm@12778
    45
    let val syms = Symbol.explode s
wenzelm@12778
    46
    in (implode (map (fn "\\" => "\\\\" | c => c) syms), real (Symbol.length syms)) end
wenzelm@12778
    47
  else (s, real (size s));
wenzelm@12778
    48
wenzelm@12778
    49
fun pgml_output (s, len) =
wenzelm@12778
    50
  if pgml () then (XML.text s, len)
wenzelm@12778
    51
  else (s, len);
wenzelm@12778
    52
wenzelm@12778
    53
in
wenzelm@12778
    54
wenzelm@12778
    55
fun setup_xsymbols_output () =
wenzelm@12778
    56
  Symbol.add_mode proof_generalN (pgml_output o xsymbols_output, Symbol.default_indent);
wenzelm@12778
    57
wenzelm@12778
    58
end;
wenzelm@12778
    59
wenzelm@12778
    60
wenzelm@12778
    61
(* token translations *)
wenzelm@12778
    62
wenzelm@12778
    63
local
wenzelm@12778
    64
wenzelm@12778
    65
val end_tag = oct_char "350";
wenzelm@12778
    66
val class_tag = ("class", oct_char "351");
wenzelm@12778
    67
val tfree_tag = ("tfree", oct_char "352");
wenzelm@12778
    68
val tvar_tag = ("tvar", oct_char "353");
wenzelm@12778
    69
val free_tag = ("free", oct_char "354");
wenzelm@12778
    70
val bound_tag = ("bound", oct_char "355");
wenzelm@12778
    71
val var_tag = ("var", oct_char "356");
wenzelm@12778
    72
val skolem_tag = ("skolem", oct_char "357");
wenzelm@12778
    73
wenzelm@12778
    74
fun xml_atom kind x = XML.element "atom" [("kind", kind)] [XML.text x];
wenzelm@12778
    75
wenzelm@12778
    76
fun tagit (kind, bg_tag) x =
wenzelm@12778
    77
  (if pgml () then xml_atom kind x else bg_tag ^ x ^ end_tag,
wenzelm@12778
    78
    real (Symbol.length (Symbol.explode x)));
wenzelm@12778
    79
wenzelm@12778
    80
fun free_or_skolem x =
wenzelm@12778
    81
  (case try Syntax.dest_skolem x of
wenzelm@12778
    82
    None => tagit free_tag x
wenzelm@12778
    83
  | Some x' => tagit skolem_tag x');
wenzelm@12778
    84
wenzelm@12778
    85
fun var_or_skolem s =
wenzelm@12778
    86
  (case Syntax.read_var s of
wenzelm@12778
    87
    Var ((x, i), _) =>
wenzelm@12778
    88
      (case try Syntax.dest_skolem x of
wenzelm@12778
    89
        None => tagit var_tag s
wenzelm@12778
    90
      | Some x' => tagit skolem_tag (Syntax.string_of_vname (x', i)))
wenzelm@12778
    91
  | _ => tagit var_tag s);
wenzelm@12778
    92
wenzelm@12778
    93
val proof_general_trans =
wenzelm@12778
    94
 Syntax.tokentrans_mode proof_generalN
wenzelm@12778
    95
  [("class", tagit class_tag),
wenzelm@12778
    96
   ("tfree", tagit tfree_tag),
wenzelm@12778
    97
   ("tvar", tagit tvar_tag),
wenzelm@12778
    98
   ("free", free_or_skolem),
wenzelm@12778
    99
   ("bound", tagit bound_tag),
wenzelm@12778
   100
   ("var", var_or_skolem)];
wenzelm@12778
   101
wenzelm@12778
   102
in val setup = [Theory.add_tokentrfuns proof_general_trans] end;
wenzelm@12778
   103
wenzelm@12778
   104
wenzelm@12778
   105
wenzelm@12778
   106
(* messages and notification *)
wenzelm@12778
   107
wenzelm@12778
   108
local
wenzelm@12778
   109
wenzelm@12778
   110
fun decorated_output bg en prfx =
wenzelm@12778
   111
  writeln_default o enclose bg en o prefix_lines prfx;
wenzelm@12778
   112
wenzelm@12778
   113
fun message kind bg en prfx s =
wenzelm@12778
   114
  if pgml () then writeln_default (XML.element kind [] [prefix_lines prfx s])
wenzelm@12778
   115
  else decorated_output bg en prfx s;
wenzelm@12778
   116
wenzelm@12778
   117
val notify = message "notify" (oct_char "360") (oct_char "361") "";
wenzelm@12778
   118
wenzelm@12778
   119
in
wenzelm@12778
   120
wenzelm@12778
   121
fun setup_messages () =
wenzelm@12778
   122
 (writeln_fn := message "output" "" "" "";
wenzelm@12778
   123
  priority_fn := message "information" (oct_char "360") (oct_char "361") "";
wenzelm@12778
   124
  tracing_fn := message "tracing" (oct_char "360" ^ oct_char "375") (oct_char "361") "";
wenzelm@12778
   125
  warning_fn := message "warning" (oct_char "362") (oct_char "363") "### ";
wenzelm@12778
   126
  error_fn := message "error" (oct_char "364") (oct_char "365") "*** ");
wenzelm@12778
   127
wenzelm@12778
   128
fun tell_clear_goals () = notify "Proof General, please clear the goals buffer.";
wenzelm@12778
   129
fun tell_clear_response () = notify "Proof General, please clear the response buffer.";
wenzelm@12778
   130
fun tell_file msg path = notify ("Proof General, " ^ msg ^ " " ^ quote (File.sysify_path path));
wenzelm@12778
   131
wenzelm@12778
   132
end;
wenzelm@12778
   133
wenzelm@12778
   134
wenzelm@12778
   135
(* theory / proof state output *)
wenzelm@12778
   136
wenzelm@12778
   137
local
wenzelm@12778
   138
wenzelm@12778
   139
fun tmp_markers f =
wenzelm@12778
   140
  setmp Display.current_goals_markers (oct_char "366", oct_char "367", "") f ();
wenzelm@12778
   141
wenzelm@12778
   142
fun statedisplay prts =
wenzelm@12778
   143
  writeln_default (XML.element "statedisplay" [] [Pretty.string_of (Pretty.chunks prts)]);
wenzelm@12778
   144
wenzelm@12778
   145
fun print_current_goals n m st =
wenzelm@12778
   146
  if pgml () then statedisplay (Display.pretty_current_goals n m st)
wenzelm@12778
   147
  else tmp_markers (fn () => Display.print_current_goals_default n m st);
wenzelm@12778
   148
wenzelm@12778
   149
fun print_state b st =
wenzelm@12778
   150
  if pgml () then statedisplay (Toplevel.pretty_state b st)
wenzelm@12778
   151
  else tmp_markers (fn () => Toplevel.print_state_default b st);
wenzelm@12778
   152
wenzelm@12778
   153
in
wenzelm@12778
   154
wenzelm@12778
   155
fun setup_state () =
wenzelm@12778
   156
 (Display.print_current_goals_fn := print_current_goals;
wenzelm@12778
   157
  Toplevel.print_state_fn := print_state;
wenzelm@12778
   158
  Toplevel.prompt_state_fn := (suffix (oct_char "372") o Toplevel.prompt_state_default));
wenzelm@12778
   159
wenzelm@12778
   160
end;
wenzelm@12778
   161
wenzelm@12778
   162
wenzelm@12778
   163
(* theory loader actions *)
wenzelm@12778
   164
wenzelm@12778
   165
local
wenzelm@12778
   166
wenzelm@12778
   167
fun add_master_files name files =
wenzelm@12778
   168
  let val masters = [ThyLoad.thy_path name, ThyLoad.ml_path name]
wenzelm@12778
   169
  in masters @ gen_rems (op = o pairself Path.base) (files, masters) end;
wenzelm@12778
   170
wenzelm@12778
   171
fun trace_action action name =
wenzelm@12778
   172
  if action = ThyInfo.Update then
wenzelm@12778
   173
    seq (tell_file "this file is loaded:") (ThyInfo.loaded_files name)
wenzelm@12778
   174
  else if action = ThyInfo.Outdate orelse action = ThyInfo.Remove then
wenzelm@12778
   175
    seq (tell_file "you can unlock the file") (add_master_files name (ThyInfo.loaded_files name))
wenzelm@12778
   176
  else ();
wenzelm@12778
   177
wenzelm@12778
   178
in
wenzelm@12778
   179
  fun setup_thy_loader () = ThyInfo.add_hook trace_action;
wenzelm@12778
   180
  fun sync_thy_loader () = seq (trace_action ThyInfo.Update) (ThyInfo.names ());
wenzelm@12778
   181
end;
wenzelm@12778
   182
wenzelm@12778
   183
wenzelm@12778
   184
(* prepare theory context *)
wenzelm@12778
   185
wenzelm@12778
   186
val thy_name = Path.pack o Path.drop_ext o Path.base o Path.unpack;
wenzelm@12778
   187
val update_thy_only = setmp MetaSimplifier.trace_simp false ThyInfo.update_thy_only;
wenzelm@12778
   188
wenzelm@12778
   189
fun which_context () =
wenzelm@12778
   190
  (case Context.get_context () of
wenzelm@12778
   191
    Some thy => "  Using current (dynamic!) one: " ^
wenzelm@12778
   192
      (case try PureThy.get_name thy of Some name => quote name | None => "<unnamed>")
wenzelm@12778
   193
  | None => "");
wenzelm@12778
   194
wenzelm@12778
   195
fun try_update_thy_only file =
wenzelm@12778
   196
  ThyLoad.cond_add_path (Path.dir (Path.unpack file)) (fn () =>
wenzelm@12778
   197
    let val name = thy_name file in
wenzelm@12778
   198
      if is_some (ThyLoad.check_file (ThyLoad.thy_path name)) then update_thy_only name
wenzelm@12778
   199
      else warning ("Unkown theory context of ML file." ^ which_context ())
wenzelm@12778
   200
    end) ();
wenzelm@12778
   201
wenzelm@12778
   202
wenzelm@12778
   203
(* get informed about files *)
wenzelm@12778
   204
wenzelm@12778
   205
val touch_child_thys = ThyInfo.if_known_thy ThyInfo.touch_child_thys;
wenzelm@12778
   206
wenzelm@12778
   207
val inform_file_processed = touch_child_thys o thy_name;
wenzelm@12778
   208
val inform_file_retracted = touch_child_thys o thy_name;
wenzelm@12778
   209
wenzelm@12778
   210
fun proper_inform_file_processed file state =
wenzelm@12778
   211
  let val name = thy_name file in
wenzelm@12778
   212
    touch_child_thys name;
wenzelm@12778
   213
    if not (Toplevel.is_toplevel state) then
wenzelm@12778
   214
      warning ("Not at toplevel -- cannot register theory " ^ quote name)
wenzelm@12778
   215
    else Library.transform_error ThyInfo.pretend_use_thy_only name handle ERROR_MESSAGE msg =>
wenzelm@12778
   216
      (warning msg; warning ("Failed to register theory " ^ quote name))
wenzelm@12778
   217
  end;
wenzelm@12778
   218
wenzelm@12778
   219
wenzelm@12778
   220
(* misc commands for ProofGeneral/isa *)
wenzelm@12778
   221
wenzelm@12778
   222
fun thms_containing ss =
wenzelm@12778
   223
  let
wenzelm@12778
   224
    val thy = the_context ();
wenzelm@12778
   225
    fun read_term s = Thm.term_of (Thm.read_cterm (Theory.sign_of thy) (s, TypeInfer.logicT));
wenzelm@12778
   226
  in ThmDatabase.print_thms_containing thy (map read_term ss) end;
wenzelm@12778
   227
wenzelm@12778
   228
val welcome = priority o Session.welcome;
wenzelm@12778
   229
val help = welcome;
wenzelm@12778
   230
val show_context = Context.the_context;
wenzelm@12778
   231
wenzelm@12778
   232
fun kill_goal () = (Goals.reset_goals (); tell_clear_goals ());
wenzelm@12778
   233
wenzelm@12778
   234
fun no_print_goals f = setmp Display.print_current_goals_fn (fn _ => fn _ => fn _ => ()) f;
wenzelm@12778
   235
wenzelm@12778
   236
fun repeat_undo 0 = ()
wenzelm@12778
   237
  | repeat_undo 1 = undo ()
wenzelm@12778
   238
  | repeat_undo n = (no_print_goals undo (); repeat_undo (n - 1));
wenzelm@12778
   239
wenzelm@12778
   240
wenzelm@12778
   241
(* restart top-level loop (keeps most state information) *)
wenzelm@12778
   242
wenzelm@12778
   243
local
wenzelm@12778
   244
wenzelm@12778
   245
fun restart isar =
wenzelm@12778
   246
 (if isar then tell_clear_goals () else kill_goal ();
wenzelm@12778
   247
  tell_clear_response ();
wenzelm@12778
   248
  welcome ());
wenzelm@12778
   249
wenzelm@12778
   250
in
wenzelm@12778
   251
wenzelm@12778
   252
fun isa_restart () = restart false;
wenzelm@12778
   253
fun isar_restart () = (sync_thy_loader (); restart true; raise Toplevel.RESTART);
wenzelm@12778
   254
wenzelm@12778
   255
end;
wenzelm@12778
   256
wenzelm@12778
   257
wenzelm@12833
   258
fun full_proofs true = proofs := 2
wenzelm@12833
   259
  | full_proofs false = proofs := 1;
wenzelm@12833
   260
wenzelm@12833
   261
wenzelm@12778
   262
(* outer syntax *)
wenzelm@12778
   263
wenzelm@12778
   264
local structure P = OuterParse and K = OuterSyntax.Keyword in
wenzelm@12778
   265
wenzelm@12778
   266
val old_undoP = (*same name for compatibility with PG/Isabelle99*)
wenzelm@12778
   267
  OuterSyntax.improper_command "undo" "undo last command (no output)" K.control
wenzelm@12778
   268
    (Scan.succeed (Toplevel.no_timing o IsarCmd.undo));
wenzelm@12778
   269
wenzelm@12778
   270
val undoP =
wenzelm@12778
   271
  OuterSyntax.improper_command "ProofGeneral.undo" "(internal)" K.control
wenzelm@12778
   272
    (Scan.succeed (Toplevel.no_timing o IsarCmd.undo));
wenzelm@12778
   273
wenzelm@12778
   274
val context_thy_onlyP =
wenzelm@12778
   275
  OuterSyntax.improper_command "ProofGeneral.context_thy_only" "(internal)" K.control
wenzelm@12778
   276
    (P.name >> (Toplevel.no_timing oo IsarThy.init_context update_thy_only));
wenzelm@12778
   277
wenzelm@12778
   278
val try_context_thy_onlyP =
wenzelm@12778
   279
  OuterSyntax.improper_command "ProofGeneral.try_context_thy_only" "(internal)" K.control
wenzelm@12778
   280
    (P.name >> (Toplevel.no_timing oo
wenzelm@12778
   281
      (Toplevel.imperative (K ()) oo IsarThy.init_context try_update_thy_only)));
wenzelm@12778
   282
wenzelm@12778
   283
val restartP =
wenzelm@12778
   284
  OuterSyntax.improper_command "ProofGeneral.restart" "(internal)" K.control
wenzelm@12778
   285
    (P.opt_unit >> (Toplevel.no_timing oo K (Toplevel.imperative isar_restart)));
wenzelm@12778
   286
wenzelm@12778
   287
val kill_proofP =
wenzelm@12778
   288
  OuterSyntax.improper_command "ProofGeneral.kill_proof" "(internal)" K.control
wenzelm@12778
   289
    (Scan.succeed (Toplevel.no_timing o IsarCmd.kill_proof_notify tell_clear_goals));
wenzelm@12778
   290
wenzelm@12778
   291
val inform_file_processedP =
wenzelm@12778
   292
  OuterSyntax.improper_command "ProofGeneral.inform_file_processed" "(internal)" K.control
wenzelm@12778
   293
    (P.name >> (Toplevel.no_timing oo
wenzelm@12778
   294
      (fn name => Toplevel.keep (proper_inform_file_processed name))));
wenzelm@12778
   295
wenzelm@12778
   296
val inform_file_retractedP =
wenzelm@12778
   297
  OuterSyntax.improper_command "ProofGeneral.inform_file_retracted" "(internal)" K.control
wenzelm@12778
   298
    (P.name >> (Toplevel.no_timing oo
wenzelm@12778
   299
      (fn name => Toplevel.imperative (fn () => inform_file_retracted name))));
wenzelm@12778
   300
wenzelm@12778
   301
fun init_outer_syntax () = OuterSyntax.add_parsers
wenzelm@12778
   302
 [old_undoP, undoP, restartP, kill_proofP, context_thy_onlyP, try_context_thy_onlyP,
wenzelm@12778
   303
  inform_file_processedP, inform_file_retractedP];
wenzelm@12778
   304
wenzelm@12778
   305
end;
wenzelm@12778
   306
wenzelm@12778
   307
wenzelm@12778
   308
(* init *)
wenzelm@12778
   309
wenzelm@12778
   310
val initialized = ref false;
wenzelm@12778
   311
wenzelm@12778
   312
fun init isar =
wenzelm@12778
   313
 (conditional (not (! initialized)) (fn () =>
wenzelm@12778
   314
   (if isar then setmp warning_fn (K ()) init_outer_syntax () else ();
wenzelm@12778
   315
    setup_xsymbols_output ();
wenzelm@12778
   316
    setup_messages ();
wenzelm@12778
   317
    setup_state ();
wenzelm@12778
   318
    setup_thy_loader ();
wenzelm@12778
   319
    set initialized; ()));
wenzelm@12778
   320
  sync_thy_loader ();
wenzelm@12778
   321
  print_mode := proof_generalN :: (! print_mode \ proof_generalN);
wenzelm@12778
   322
  set quick_and_dirty;
wenzelm@12778
   323
  ThmDeps.enable ();
wenzelm@12778
   324
  if isar then ml_prompts "ML> " "ML# "
wenzelm@12778
   325
  else ml_prompts ("> " ^ oct_char "372") ("- " ^ oct_char "373");
wenzelm@12778
   326
  if isar then (welcome (); Isar.sync_main ()) else isa_restart ());
wenzelm@12778
   327
wenzelm@12778
   328
wenzelm@12778
   329
wenzelm@12778
   330
(** generate keyword classification file **)
wenzelm@12778
   331
wenzelm@12778
   332
local
wenzelm@12778
   333
wenzelm@12778
   334
val regexp_meta = explode ".*+?[]^$";
wenzelm@12778
   335
val regexp_quote = implode o map (fn c => if c mem regexp_meta then "\\\\" ^ c else c) o explode;
wenzelm@12778
   336
wenzelm@12778
   337
fun defconst name strs =
wenzelm@12778
   338
  "\n(defconst isar-keywords-" ^ name ^
wenzelm@12778
   339
  "\n  '(" ^ space_implode "\n    " (map (quote o regexp_quote) strs) ^ "))\n";
wenzelm@12778
   340
wenzelm@12778
   341
fun make_elisp_commands commands kind =
wenzelm@12778
   342
  defconst kind (mapfilter (fn (c, _, k, _) => if k = kind then Some c else None) commands);
wenzelm@12778
   343
wenzelm@12778
   344
fun make_elisp_syntax (keywords, commands) =
wenzelm@12778
   345
  ";;\n\
wenzelm@12778
   346
  \;; Keyword classification tables for Isabelle/Isar.\n\
wenzelm@12778
   347
  \;; This file was generated by " ^ Session.name () ^ " -- DO NOT EDIT!\n\
wenzelm@12778
   348
  \;;\n\
wenzelm@12778
   349
  \;; $" ^ "Id$\n\
wenzelm@12778
   350
  \;;\n" ^
wenzelm@12778
   351
  defconst "major" (map #1 commands) ^
wenzelm@12778
   352
  defconst "minor" (filter Syntax.is_identifier keywords) ^
wenzelm@12778
   353
  implode (map (make_elisp_commands commands) OuterSyntax.Keyword.kinds) ^
wenzelm@12778
   354
  "\n(provide 'isar-keywords)\n";
wenzelm@12778
   355
wenzelm@12778
   356
in
wenzelm@12778
   357
wenzelm@12778
   358
fun write_keywords s =
wenzelm@12778
   359
  (init_outer_syntax ();
wenzelm@12778
   360
    File.write (Path.unpack ("isar-keywords" ^ (if s = "" then "" else "-" ^ s) ^".el"))
wenzelm@12778
   361
      (make_elisp_syntax (OuterSyntax.dest_keywords (), OuterSyntax.dest_parsers ())));
wenzelm@12778
   362
wenzelm@12778
   363
end;
wenzelm@12778
   364
wenzelm@12778
   365
wenzelm@12778
   366
end;
wenzelm@12778
   367
wenzelm@12778
   368
(*a hack for Proof General 3.2 to avoid problems with escapes in ML commands*)
wenzelm@12778
   369
infix \\\\ val op \\\\ = op \\;