src/Pure/proof_general.ML
author wenzelm
Sat, 29 May 2004 15:02:35 +0200
changeset 14827 d973e7f820cb
parent 14725 2ed5b960c6b1
child 14880 7586233bd4bd
permissions -rw-r--r--
Output.add_mode; Output.timing;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
12780
6b41c750451c tuned title;
wenzelm
parents: 12778
diff changeset
     1
(*  Title:      Pure/proof_general.ML
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
14675
08b9c690f9cf removed obsolete 'undo';
wenzelm
parents: 14568
diff changeset
     3
    Author:     David Aspinall and Markus Wenzel
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
     5
14566
0b60b2edce03 corrected PG url in comment
nipkow
parents: 14561
diff changeset
     6
Isabelle configuration for Proof General (see http://proofgeneral.inf.ed.ac.uk).
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
     7
*)
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
     8
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
     9
signature PROOF_GENERAL =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    10
sig
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    11
  val setup: (theory -> theory) list
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    12
  val update_thy_only: string -> unit
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    13
  val try_update_thy_only: string -> unit
13391
553e7b62680f fixed inform_file_retracted: remove_thy;
wenzelm
parents: 13284
diff changeset
    14
  val inform_file_retracted: string -> unit
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    15
  val inform_file_processed: string -> unit
13728
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
    16
  val options: (string * (string * (string * (unit -> string) * (string -> unit)))) list ref
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
    17
  val process_pgip: string -> unit
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    18
  val thms_containing: string list -> unit
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    19
  val help: unit -> unit
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    20
  val show_context: unit -> theory
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    21
  val kill_goal: unit -> unit
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    22
  val repeat_undo: int -> unit
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    23
  val isa_restart: unit -> unit
12833
9f3226cfe021 full_proofs;
wenzelm
parents: 12780
diff changeset
    24
  val full_proofs: bool -> unit
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    25
  val init: bool -> unit
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    26
  val write_keywords: string -> unit
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    27
end;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    28
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    29
structure ProofGeneral: PROOF_GENERAL =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    30
struct
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    31
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    32
(* print modes *)
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    33
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    34
val proof_generalN = "ProofGeneral";
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    35
val xsymbolsN = "xsymbols";
13538
wenzelm
parents: 13526
diff changeset
    36
val thm_depsN = "thm_deps";
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    37
13728
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
    38
val pgml_version_supported = "1.0";
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    39
val pgmlN = "PGML";
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    40
fun pgml () = pgmlN mem_string ! print_mode;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    41
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    42
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    43
(* text output *)
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    44
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    45
local
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    46
14827
d973e7f820cb Output.add_mode; Output.timing;
wenzelm
parents: 14725
diff changeset
    47
fun xsym_output "\\" = "\\\\"
d973e7f820cb Output.add_mode; Output.timing;
wenzelm
parents: 14725
diff changeset
    48
  | xsym_output s = if Symbol.is_raw s then Symbol.decode_raw s else s;
d973e7f820cb Output.add_mode; Output.timing;
wenzelm
parents: 14725
diff changeset
    49
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    50
fun xsymbols_output s =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    51
  if xsymbolsN mem_string ! print_mode andalso exists_string (equal "\\") s then
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    52
    let val syms = Symbol.explode s
14827
d973e7f820cb Output.add_mode; Output.timing;
wenzelm
parents: 14725
diff changeset
    53
    in (implode (map xsym_output syms), real (Symbol.length syms)) end
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    54
  else (s, real (size s));
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    55
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    56
fun pgml_output (s, len) =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    57
  if pgml () then (XML.text s, len)
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    58
  else (s, len);
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    59
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    60
in
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    61
14827
d973e7f820cb Output.add_mode; Output.timing;
wenzelm
parents: 14725
diff changeset
    62
fun setup_xsymbols_output () = Output.add_mode proof_generalN
d973e7f820cb Output.add_mode; Output.timing;
wenzelm
parents: 14725
diff changeset
    63
  (pgml_output o xsymbols_output, Symbol.default_indent, Symbol.default_raw);
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    64
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    65
end;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    66
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    67
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    68
(* token translations *)
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    69
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    70
local
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    71
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    72
val end_tag = oct_char "350";
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    73
val class_tag = ("class", oct_char "351");
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    74
val tfree_tag = ("tfree", oct_char "352");
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    75
val tvar_tag = ("tvar", oct_char "353");
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    76
val free_tag = ("free", oct_char "354");
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    77
val bound_tag = ("bound", oct_char "355");
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    78
val var_tag = ("var", oct_char "356");
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    79
val skolem_tag = ("skolem", oct_char "357");
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    80
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    81
fun xml_atom kind x = XML.element "atom" [("kind", kind)] [XML.text x];
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    82
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    83
fun tagit (kind, bg_tag) x =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    84
  (if pgml () then xml_atom kind x else bg_tag ^ x ^ end_tag,
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    85
    real (Symbol.length (Symbol.explode x)));
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    86
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    87
fun free_or_skolem x =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    88
  (case try Syntax.dest_skolem x of
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    89
    None => tagit free_tag x
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    90
  | Some x' => tagit skolem_tag x');
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    91
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    92
fun var_or_skolem s =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    93
  (case Syntax.read_var s of
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    94
    Var ((x, i), _) =>
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    95
      (case try Syntax.dest_skolem x of
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    96
        None => tagit var_tag s
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    97
      | Some x' => tagit skolem_tag (Syntax.string_of_vname (x', i)))
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    98
  | _ => tagit var_tag s);
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    99
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   100
val proof_general_trans =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   101
 Syntax.tokentrans_mode proof_generalN
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   102
  [("class", tagit class_tag),
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   103
   ("tfree", tagit tfree_tag),
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   104
   ("tvar", tagit tvar_tag),
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   105
   ("free", free_or_skolem),
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   106
   ("bound", tagit bound_tag),
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   107
   ("var", var_or_skolem)];
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   108
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   109
in val setup = [Theory.add_tokentrfuns proof_general_trans] end;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   110
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   111
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   112
(* messages and notification *)
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   113
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   114
local
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   115
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   116
fun decorated_output bg en prfx =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   117
  writeln_default o enclose bg en o prefix_lines prfx;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   118
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   119
fun message kind bg en prfx s =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   120
  if pgml () then writeln_default (XML.element kind [] [prefix_lines prfx s])
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   121
  else decorated_output bg en prfx s;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   122
13526
9269275e5da6 result dependency output;
wenzelm
parents: 13391
diff changeset
   123
in
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   124
13526
9269275e5da6 result dependency output;
wenzelm
parents: 13391
diff changeset
   125
val notify = message "notify" (oct_char "360") (oct_char "361") "";
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   126
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   127
fun setup_messages () =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   128
 (writeln_fn := message "output" "" "" "";
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   129
  priority_fn := message "information" (oct_char "360") (oct_char "361") "";
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   130
  tracing_fn := message "tracing" (oct_char "360" ^ oct_char "375") (oct_char "361") "";
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   131
  warning_fn := message "warning" (oct_char "362") (oct_char "363") "### ";
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   132
  error_fn := message "error" (oct_char "364") (oct_char "365") "*** ");
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   133
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   134
fun tell_clear_goals () = notify "Proof General, please clear the goals buffer.";
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   135
fun tell_clear_response () = notify "Proof General, please clear the response buffer.";
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   136
fun tell_file msg path = notify ("Proof General, " ^ msg ^ " " ^ quote (File.sysify_path path));
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   137
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   138
end;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   139
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   140
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   141
(* theory / proof state output *)
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   142
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   143
local
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   144
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   145
fun tmp_markers f =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   146
  setmp Display.current_goals_markers (oct_char "366", oct_char "367", "") f ();
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   147
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   148
fun statedisplay prts =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   149
  writeln_default (XML.element "statedisplay" [] [Pretty.string_of (Pretty.chunks prts)]);
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   150
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   151
fun print_current_goals n m st =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   152
  if pgml () then statedisplay (Display.pretty_current_goals n m st)
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   153
  else tmp_markers (fn () => Display.print_current_goals_default n m st);
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   154
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   155
fun print_state b st =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   156
  if pgml () then statedisplay (Toplevel.pretty_state b st)
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   157
  else tmp_markers (fn () => Toplevel.print_state_default b st);
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   158
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   159
in
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   160
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   161
fun setup_state () =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   162
 (Display.print_current_goals_fn := print_current_goals;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   163
  Toplevel.print_state_fn := print_state;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   164
  Toplevel.prompt_state_fn := (suffix (oct_char "372") o Toplevel.prompt_state_default));
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   165
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   166
end;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   167
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   168
13538
wenzelm
parents: 13526
diff changeset
   169
(* theorem dependency output *)
13526
9269275e5da6 result dependency output;
wenzelm
parents: 13391
diff changeset
   170
9269275e5da6 result dependency output;
wenzelm
parents: 13391
diff changeset
   171
local
9269275e5da6 result dependency output;
wenzelm
parents: 13391
diff changeset
   172
13545
fcdbd6cf5f9f improved tell_thm_deps;
wenzelm
parents: 13538
diff changeset
   173
val spaces_quote = space_implode " " o map quote;
fcdbd6cf5f9f improved tell_thm_deps;
wenzelm
parents: 13538
diff changeset
   174
13526
9269275e5da6 result dependency output;
wenzelm
parents: 13391
diff changeset
   175
fun tell_thm_deps ths =
13538
wenzelm
parents: 13526
diff changeset
   176
  conditional (thm_depsN mem_string ! print_mode) (fn () =>
wenzelm
parents: 13526
diff changeset
   177
    let
13545
fcdbd6cf5f9f improved tell_thm_deps;
wenzelm
parents: 13538
diff changeset
   178
      val names = map Thm.name_of_thm ths \ "";
fcdbd6cf5f9f improved tell_thm_deps;
wenzelm
parents: 13538
diff changeset
   179
      val deps = Symtab.keys (foldl (uncurry Proofterm.thms_of_proof)
fcdbd6cf5f9f improved tell_thm_deps;
wenzelm
parents: 13538
diff changeset
   180
          (Symtab.empty, map Thm.proof_of ths)) \ "";
13538
wenzelm
parents: 13526
diff changeset
   181
    in
13545
fcdbd6cf5f9f improved tell_thm_deps;
wenzelm
parents: 13538
diff changeset
   182
      if null names orelse null deps then ()
fcdbd6cf5f9f improved tell_thm_deps;
wenzelm
parents: 13538
diff changeset
   183
      else notify ("Proof General, theorem dependencies of " ^ spaces_quote names ^ " are "
fcdbd6cf5f9f improved tell_thm_deps;
wenzelm
parents: 13538
diff changeset
   184
        ^ spaces_quote deps)
13538
wenzelm
parents: 13526
diff changeset
   185
    end);
13526
9269275e5da6 result dependency output;
wenzelm
parents: 13391
diff changeset
   186
9269275e5da6 result dependency output;
wenzelm
parents: 13391
diff changeset
   187
in
9269275e5da6 result dependency output;
wenzelm
parents: 13391
diff changeset
   188
9269275e5da6 result dependency output;
wenzelm
parents: 13391
diff changeset
   189
fun setup_present_hook () =
9269275e5da6 result dependency output;
wenzelm
parents: 13391
diff changeset
   190
  Present.add_hook (fn _ => fn res => tell_thm_deps (flat (map #2 res)));
9269275e5da6 result dependency output;
wenzelm
parents: 13391
diff changeset
   191
9269275e5da6 result dependency output;
wenzelm
parents: 13391
diff changeset
   192
end;
9269275e5da6 result dependency output;
wenzelm
parents: 13391
diff changeset
   193
9269275e5da6 result dependency output;
wenzelm
parents: 13391
diff changeset
   194
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   195
(* theory loader actions *)
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   196
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   197
local
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   198
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   199
fun add_master_files name files =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   200
  let val masters = [ThyLoad.thy_path name, ThyLoad.ml_path name]
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   201
  in masters @ gen_rems (op = o pairself Path.base) (files, masters) end;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   202
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   203
fun trace_action action name =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   204
  if action = ThyInfo.Update then
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   205
    seq (tell_file "this file is loaded:") (ThyInfo.loaded_files name)
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   206
  else if action = ThyInfo.Outdate orelse action = ThyInfo.Remove then
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   207
    seq (tell_file "you can unlock the file") (add_master_files name (ThyInfo.loaded_files name))
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   208
  else ();
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   209
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   210
in
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   211
  fun setup_thy_loader () = ThyInfo.add_hook trace_action;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   212
  fun sync_thy_loader () = seq (trace_action ThyInfo.Update) (ThyInfo.names ());
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   213
end;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   214
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   215
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   216
(* prepare theory context *)
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   217
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   218
val thy_name = Path.pack o Path.drop_ext o Path.base o Path.unpack;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   219
val update_thy_only = setmp MetaSimplifier.trace_simp false ThyInfo.update_thy_only;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   220
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   221
fun which_context () =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   222
  (case Context.get_context () of
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   223
    Some thy => "  Using current (dynamic!) one: " ^
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   224
      (case try PureThy.get_name thy of Some name => quote name | None => "<unnamed>")
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   225
  | None => "");
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   226
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   227
fun try_update_thy_only file =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   228
  ThyLoad.cond_add_path (Path.dir (Path.unpack file)) (fn () =>
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   229
    let val name = thy_name file in
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   230
      if is_some (ThyLoad.check_file (ThyLoad.thy_path name)) then update_thy_only name
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   231
      else warning ("Unkown theory context of ML file." ^ which_context ())
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   232
    end) ();
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   233
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   234
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   235
(* get informed about files *)
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   236
13391
553e7b62680f fixed inform_file_retracted: remove_thy;
wenzelm
parents: 13284
diff changeset
   237
val inform_file_retracted = ThyInfo.if_known_thy ThyInfo.remove_thy o thy_name;
553e7b62680f fixed inform_file_retracted: remove_thy;
wenzelm
parents: 13284
diff changeset
   238
val inform_file_processed = ThyInfo.if_known_thy ThyInfo.touch_child_thys o thy_name;
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   239
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   240
fun proper_inform_file_processed file state =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   241
  let val name = thy_name file in
13391
553e7b62680f fixed inform_file_retracted: remove_thy;
wenzelm
parents: 13284
diff changeset
   242
    ThyInfo.if_known_thy ThyInfo.touch_child_thys name;
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   243
    if not (Toplevel.is_toplevel state) then
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   244
      warning ("Not at toplevel -- cannot register theory " ^ quote name)
14827
d973e7f820cb Output.add_mode; Output.timing;
wenzelm
parents: 14725
diff changeset
   245
    else transform_error ThyInfo.pretend_use_thy_only name handle ERROR_MESSAGE msg =>
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   246
      (warning msg; warning ("Failed to register theory " ^ quote name))
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   247
  end;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   248
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   249
13728
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   250
(* options *)
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   251
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   252
fun nat_option r = ("nat",
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   253
  (fn () => string_of_int (!r)),
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   254
  (fn s => (case Syntax.read_nat s of
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   255
       None => error "nat_option: illegal value"
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   256
     | Some i => r := i)));
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   257
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   258
fun bool_option r = ("boolean",
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   259
  (fn () => Bool.toString (!r)),
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   260
  (fn "false" => r := false | "true" => r := true
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   261
    | _ => error "bool_option: illegal value"));
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   262
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   263
val proof_option = ("boolean",
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   264
  (fn () => Bool.toString (!proofs >= 2)),
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   265
  (fn "false" => proofs := 1 | "true" => proofs := 2
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   266
    | _ => error "proof_option: illegal value"));
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   267
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   268
val thm_deps_option = ("boolean",
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   269
  (fn () => Bool.toString ("thm_deps" mem !print_mode)),
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   270
  (fn "false" => print_mode := Library.gen_rems (op =) (!print_mode, ["thm_deps"])
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   271
    | "true" => print_mode := (["thm_deps"] @ !print_mode)
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   272
    | _ => error "thm_deps_option: illegal value"));
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   273
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   274
val print_depth_option = ("nat",
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   275
  (fn () => "10"),
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   276
  (fn s => (case Syntax.read_nat s of
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   277
       None => error "print_depth_option: illegal value"
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   278
     | Some i => print_depth i)));
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   279
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   280
val options = ref
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   281
  [("show-types", ("Whether to show types in Isabelle.",
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   282
      bool_option show_types)),
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   283
   ("show-sorts", ("Whether to show sorts in Isabelle.",
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   284
      bool_option show_sorts)),
14707
2d6350d7b9b7 show_structs option;
wenzelm
parents: 14675
diff changeset
   285
   ("show-structs", ("Whether to show implicit structures in Isabelle.",
2d6350d7b9b7 show_structs option;
wenzelm
parents: 14675
diff changeset
   286
      bool_option show_structs)),
13728
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   287
   ("show-consts", ("Whether to show types of consts in Isabelle goals.",
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   288
      bool_option show_consts)),
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   289
   ("long-names", ("Whether to show fully qualified names in Isabelle.",
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   290
      bool_option long_names)),
13884
5affbaee6b18 Added show_brackets to settings menu.
berghofe
parents: 13801
diff changeset
   291
   ("show-brackets", ("Whether to show full bracketing in Isabelle.",
5affbaee6b18 Added show_brackets to settings menu.
berghofe
parents: 13801
diff changeset
   292
      bool_option show_brackets)),
13728
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   293
   ("eta-contract", ("Whether to print terms eta-contracted in Isabelle.",
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   294
      bool_option Syntax.eta_contract)),
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   295
   ("trace-simplifier", ("Whether to trace the Simplifier in Isabelle.",
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   296
      bool_option trace_simp)),
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   297
   ("trace-rules", ("Whether to trace the standard rules in Isabelle.",
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   298
      bool_option trace_rules)),
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   299
   ("quick-and-dirty", ("Whether to take a few short cuts occasionally.",
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   300
      bool_option quick_and_dirty)),
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   301
   ("full-proofs", ("Whether to record full proof objects internally.",
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   302
      proof_option)),
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   303
   ("trace-unification", ("Whether to output error diagnostics during unification.",
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   304
      bool_option Pattern.trace_unify_fail)),
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   305
   ("show-main-goal", ("Whether to show main goal.",
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   306
      bool_option Proof.show_main_goal)),
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   307
   ("global-timing", ("Whether to enable timing in Isabelle.",
14827
d973e7f820cb Output.add_mode; Output.timing;
wenzelm
parents: 14725
diff changeset
   308
      bool_option Output.timing)),
13728
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   309
   ("theorem-dependencies", ("Whether to track theorem dependencies within Proof General.",
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   310
      thm_deps_option)),
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   311
   ("goals-limit", ("Setting for maximum number of goals printed in Isabelle.",
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   312
      nat_option goals_limit)),
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   313
   ("prems-limit", ("Setting for maximum number of premises printed in Isabelle/Isar.",
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   314
      nat_option ProofContext.prems_limit)),
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   315
   ("print-depth", ("Setting for the ML print depth in Isabelle.",
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   316
      print_depth_option))];
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   317
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   318
14675
08b9c690f9cf removed obsolete 'undo';
wenzelm
parents: 14568
diff changeset
   319
(* sending PGIP commands to the interface *)
13728
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   320
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   321
fun issue_pgip pgips = notify (XML.element "pgip" [] pgips);
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   322
14725
2ed5b960c6b1 ProofGeneral.process_pgip command;
wenzelm
parents: 14707
diff changeset
   323
fun usespgml () =
13728
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   324
  issue_pgip [XML.element "usespgml" [("version", pgml_version_supported)] []];
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   325
14675
08b9c690f9cf removed obsolete 'undo';
wenzelm
parents: 14568
diff changeset
   326
(*NB: the default returned here is actually the current value, so
08b9c690f9cf removed obsolete 'undo';
wenzelm
parents: 14568
diff changeset
   327
  repeated uses of <askprefs> will not work correctly*)
14725
2ed5b960c6b1 ProofGeneral.process_pgip command;
wenzelm
parents: 14707
diff changeset
   328
fun show_options () = issue_pgip (map
14568
1acde8c39179 "haspref" -> "oldhaspref" (David Aspinall)
nipkow
parents: 14567
diff changeset
   329
  (fn (name, (descr, (ty, get, _))) => (XML.element "oldhaspref"
13728
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   330
    [("type", ty), ("descr", descr), ("default", get ())] [name])) (!options));
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   331
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   332
fun set_option name value = (case assoc (!options, name) of
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   333
      None => warning ("Unknown option: " ^ quote name)
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   334
    | Some (_, (_, _, set)) => set value);
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   335
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   336
fun get_option name = (case assoc (!options, name) of
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   337
      None => warning ("Unknown option: " ^ quote name)
14725
2ed5b960c6b1 ProofGeneral.process_pgip command;
wenzelm
parents: 14707
diff changeset
   338
    | Some (_, (_, get, _)) =>
2ed5b960c6b1 ProofGeneral.process_pgip command;
wenzelm
parents: 14707
diff changeset
   339
        issue_pgip [XML.element "prefval" [("name", name)] [get ()]]);
13728
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   340
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   341
14675
08b9c690f9cf removed obsolete 'undo';
wenzelm
parents: 14568
diff changeset
   342
(* processing PGIP commands from the interface *)
13728
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   343
14675
08b9c690f9cf removed obsolete 'undo';
wenzelm
parents: 14568
diff changeset
   344
(*FIXME: matching on attributes is a bit too strict here*)
13728
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   345
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   346
fun process_pgip_element pgip = (case pgip of
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   347
      XML.Elem ("askpgml", _, []) => usespgml ()
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   348
    | XML.Elem ("askprefs", _, [])  => show_options ()
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   349
    | XML.Elem ("getpref", [("name", name)], []) => get_option name
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   350
    | XML.Elem ("setpref", [("name", name)], [XML.Text value]) =>
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   351
        set_option name value
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   352
    | XML.Elem (e, _, _) => warning ("Unrecognized PGIP command: " ^ e)
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   353
    | XML.Text t => warning ("Unrecognized PGIP command:\n" ^ t));
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   354
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   355
fun process_pgip s = (case XML.tree_of_string s of
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   356
    XML.Elem ("pgip", _, pgips) => seq process_pgip_element pgips
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   357
  | _ => warning ("Invalid PGIP packet received\n" ^ s));
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   358
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   359
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   360
(* misc commands for ProofGeneral/isa *)
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   361
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   362
fun thms_containing ss =
13284
20c818c966e6 thms_containing: optional limit argument;
wenzelm
parents: 13273
diff changeset
   363
  ProofContext.print_thms_containing (ProofContext.init (the_context ())) None ss;
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   364
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   365
val welcome = priority o Session.welcome;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   366
val help = welcome;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   367
val show_context = Context.the_context;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   368
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   369
fun kill_goal () = (Goals.reset_goals (); tell_clear_goals ());
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   370
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   371
fun no_print_goals f = setmp Display.print_current_goals_fn (fn _ => fn _ => fn _ => ()) f;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   372
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   373
fun repeat_undo 0 = ()
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   374
  | repeat_undo 1 = undo ()
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   375
  | repeat_undo n = (no_print_goals undo (); repeat_undo (n - 1));
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   376
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   377
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   378
(* restart top-level loop (keeps most state information) *)
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   379
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   380
local
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   381
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   382
fun restart isar =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   383
 (if isar then tell_clear_goals () else kill_goal ();
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   384
  tell_clear_response ();
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   385
  welcome ());
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   386
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   387
in
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   388
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   389
fun isa_restart () = restart false;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   390
fun isar_restart () = (sync_thy_loader (); restart true; raise Toplevel.RESTART);
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   391
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   392
end;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   393
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   394
12833
9f3226cfe021 full_proofs;
wenzelm
parents: 12780
diff changeset
   395
fun full_proofs true = proofs := 2
9f3226cfe021 full_proofs;
wenzelm
parents: 12780
diff changeset
   396
  | full_proofs false = proofs := 1;
9f3226cfe021 full_proofs;
wenzelm
parents: 12780
diff changeset
   397
9f3226cfe021 full_proofs;
wenzelm
parents: 12780
diff changeset
   398
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   399
(* outer syntax *)
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   400
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   401
local structure P = OuterParse and K = OuterSyntax.Keyword in
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   402
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   403
val undoP =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   404
  OuterSyntax.improper_command "ProofGeneral.undo" "(internal)" K.control
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   405
    (Scan.succeed (Toplevel.no_timing o IsarCmd.undo));
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   406
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   407
val context_thy_onlyP =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   408
  OuterSyntax.improper_command "ProofGeneral.context_thy_only" "(internal)" K.control
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   409
    (P.name >> (Toplevel.no_timing oo IsarThy.init_context update_thy_only));
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   410
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   411
val try_context_thy_onlyP =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   412
  OuterSyntax.improper_command "ProofGeneral.try_context_thy_only" "(internal)" K.control
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   413
    (P.name >> (Toplevel.no_timing oo
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   414
      (Toplevel.imperative (K ()) oo IsarThy.init_context try_update_thy_only)));
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   415
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   416
val restartP =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   417
  OuterSyntax.improper_command "ProofGeneral.restart" "(internal)" K.control
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   418
    (P.opt_unit >> (Toplevel.no_timing oo K (Toplevel.imperative isar_restart)));
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   419
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   420
val kill_proofP =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   421
  OuterSyntax.improper_command "ProofGeneral.kill_proof" "(internal)" K.control
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   422
    (Scan.succeed (Toplevel.no_timing o IsarCmd.kill_proof_notify tell_clear_goals));
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   423
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   424
val inform_file_processedP =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   425
  OuterSyntax.improper_command "ProofGeneral.inform_file_processed" "(internal)" K.control
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   426
    (P.name >> (Toplevel.no_timing oo
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   427
      (fn name => Toplevel.keep (proper_inform_file_processed name))));
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   428
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   429
val inform_file_retractedP =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   430
  OuterSyntax.improper_command "ProofGeneral.inform_file_retracted" "(internal)" K.control
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   431
    (P.name >> (Toplevel.no_timing oo
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   432
      (fn name => Toplevel.imperative (fn () => inform_file_retracted name))));
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   433
14725
2ed5b960c6b1 ProofGeneral.process_pgip command;
wenzelm
parents: 14707
diff changeset
   434
val process_pgipP =
2ed5b960c6b1 ProofGeneral.process_pgip command;
wenzelm
parents: 14707
diff changeset
   435
  OuterSyntax.improper_command "ProofGeneral.process_pgip" "(internal)" K.control
2ed5b960c6b1 ProofGeneral.process_pgip command;
wenzelm
parents: 14707
diff changeset
   436
    (P.text >> (Toplevel.no_timing oo
2ed5b960c6b1 ProofGeneral.process_pgip command;
wenzelm
parents: 14707
diff changeset
   437
      (fn txt => Toplevel.imperative (fn () => process_pgip txt))));
2ed5b960c6b1 ProofGeneral.process_pgip command;
wenzelm
parents: 14707
diff changeset
   438
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   439
fun init_outer_syntax () = OuterSyntax.add_parsers
14675
08b9c690f9cf removed obsolete 'undo';
wenzelm
parents: 14568
diff changeset
   440
 [undoP, restartP, kill_proofP, context_thy_onlyP, try_context_thy_onlyP,
14725
2ed5b960c6b1 ProofGeneral.process_pgip command;
wenzelm
parents: 14707
diff changeset
   441
  inform_file_processedP, inform_file_retractedP, process_pgipP];
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   442
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   443
end;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   444
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   445
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   446
(* init *)
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   447
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   448
val initialized = ref false;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   449
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   450
fun init isar =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   451
 (conditional (not (! initialized)) (fn () =>
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   452
   (if isar then setmp warning_fn (K ()) init_outer_syntax () else ();
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   453
    setup_xsymbols_output ();
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   454
    setup_messages ();
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   455
    setup_state ();
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   456
    setup_thy_loader ();
13526
9269275e5da6 result dependency output;
wenzelm
parents: 13391
diff changeset
   457
    setup_present_hook ();
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   458
    set initialized; ()));
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   459
  sync_thy_loader ();
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   460
  print_mode := proof_generalN :: (! print_mode \ proof_generalN);
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   461
  set quick_and_dirty;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   462
  ThmDeps.enable ();
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   463
  if isar then ml_prompts "ML> " "ML# "
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   464
  else ml_prompts ("> " ^ oct_char "372") ("- " ^ oct_char "373");
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   465
  if isar then (welcome (); Isar.sync_main ()) else isa_restart ());
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   466
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   467
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   468
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   469
(** generate keyword classification file **)
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   470
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   471
local
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   472
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   473
val regexp_meta = explode ".*+?[]^$";
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   474
val regexp_quote = implode o map (fn c => if c mem regexp_meta then "\\\\" ^ c else c) o explode;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   475
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   476
fun defconst name strs =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   477
  "\n(defconst isar-keywords-" ^ name ^
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   478
  "\n  '(" ^ space_implode "\n    " (map (quote o regexp_quote) strs) ^ "))\n";
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   479
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   480
fun make_elisp_commands commands kind =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   481
  defconst kind (mapfilter (fn (c, _, k, _) => if k = kind then Some c else None) commands);
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   482
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   483
fun make_elisp_syntax (keywords, commands) =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   484
  ";;\n\
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   485
  \;; Keyword classification tables for Isabelle/Isar.\n\
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   486
  \;; This file was generated by " ^ Session.name () ^ " -- DO NOT EDIT!\n\
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   487
  \;;\n\
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   488
  \;; $" ^ "Id$\n\
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   489
  \;;\n" ^
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   490
  defconst "major" (map #1 commands) ^
14675
08b9c690f9cf removed obsolete 'undo';
wenzelm
parents: 14568
diff changeset
   491
  defconst "minor" (filter Syntax.is_ascii_identifier keywords) ^
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   492
  implode (map (make_elisp_commands commands) OuterSyntax.Keyword.kinds) ^
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   493
  "\n(provide 'isar-keywords)\n";
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   494
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   495
in
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   496
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   497
fun write_keywords s =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   498
  (init_outer_syntax ();
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   499
    File.write (Path.unpack ("isar-keywords" ^ (if s = "" then "" else "-" ^ s) ^".el"))
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   500
      (make_elisp_syntax (OuterSyntax.dest_keywords (), OuterSyntax.dest_parsers ())));
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   501
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   502
end;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   503
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   504
end;