src/Pure/ProofGeneral/proof_general_emacs.ML
author wenzelm
Thu, 15 Nov 2007 11:49:04 +0100
changeset 25436 ca46d8a66b69
parent 25192 b568f8c5d5ca
child 25442 0337e3df3187
permissions -rw-r--r--
thy_name: be very liberal about file name format (workaround problem with XEmacs on cygwin);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
21642
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
     1
(*  Title:      Pure/ProofGeneral/proof_general_emacs.ML
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
     2
    ID:         $Id$
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
     3
    Author:     David Aspinall and Markus Wenzel
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
     4
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
     5
Isabelle/Isar configuration for Emacs Proof General.
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
     6
See http://proofgeneral.inf.ed.ac.uk
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
     7
*)
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
     8
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
     9
signature PROOF_GENERAL =
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    10
sig
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    11
  val init: bool -> unit
24874
e4400a70eeaa export init_outer_syntax;
wenzelm
parents: 24873
diff changeset
    12
  val init_outer_syntax: unit -> unit
24289
bfd59eb6e24e added sendback;
wenzelm
parents: 24244
diff changeset
    13
  val sendback: string -> Pretty.T list -> unit
21642
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    14
end;
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    15
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    16
structure ProofGeneral: PROOF_GENERAL =
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    17
struct
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    18
21945
wenzelm
parents: 21940
diff changeset
    19
21642
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    20
(* print modes *)
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    21
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    22
val proof_generalN = "ProofGeneralEmacs";  (*token markup (colouring vars, etc.)*)
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    23
val pgasciiN = "PGASCII";                  (*plain 7-bit ASCII communication*)
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    24
val thm_depsN = "thm_deps";                (*meta-information about theorem deps*)
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    25
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    26
fun special oct =
22590
ac84debdd7d3 removed unused info channel;
wenzelm
parents: 22228
diff changeset
    27
  if print_mode_active pgasciiN then chr 1 ^ chr (ord (oct_char oct) - 167)
21642
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    28
  else oct_char oct;
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    29
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    30
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    31
(* text output: print modes for xsymbol *)
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    32
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    33
local
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    34
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    35
fun xsym_output "\\" = "\\\\"
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    36
  | xsym_output s = if Symbol.is_raw s then Symbol.decode_raw s else s;
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    37
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    38
fun xsymbols_output s =
22590
ac84debdd7d3 removed unused info channel;
wenzelm
parents: 22228
diff changeset
    39
  if print_mode_active Symbol.xsymbolsN andalso exists_string (equal "\\") s then
21642
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    40
    let val syms = Symbol.explode s
23621
e070a6ab1891 simplified pretty token metric: type int;
wenzelm
parents: 22699
diff changeset
    41
    in (implode (map xsym_output syms), Symbol.length syms) end
e070a6ab1891 simplified pretty token metric: type int;
wenzelm
parents: 22699
diff changeset
    42
  else Output.default_output s;
21642
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    43
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    44
in
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    45
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    46
fun setup_xsymbols_output () =
23641
d6f9d3acffaa toplevel prompt/print_state: proper markup, removed hooks;
wenzelm
parents: 23621
diff changeset
    47
  Output.add_mode Symbol.xsymbolsN xsymbols_output Symbol.encode_raw;
21642
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    48
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    49
end;
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    50
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    51
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    52
(* token translations *)
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    53
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    54
local
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    55
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    56
fun end_tag () = special "350";
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    57
val class_tag = ("class", fn () => special "351");
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    58
val tfree_tag = ("tfree", fn () => special "352");
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    59
val tvar_tag = ("tvar", fn () => special "353");
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    60
val free_tag = ("free", fn () => special "354");
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    61
val bound_tag = ("bound", fn () => special "355");
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    62
val var_tag = ("var", fn () => special "356");
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    63
val skolem_tag = ("skolem", fn () => special "357");
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    64
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    65
fun xml_atom kind x = XML.element "atom" [("kind", kind)] [XML.text x];
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    66
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    67
fun tagit (kind, bg_tag) x =
23621
e070a6ab1891 simplified pretty token metric: type int;
wenzelm
parents: 22699
diff changeset
    68
  (bg_tag () ^ x ^ end_tag (), Symbol.length (Symbol.explode x));
21642
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    69
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    70
fun free_or_skolem x =
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    71
  (case try Name.dest_skolem x of
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    72
    NONE => tagit free_tag x
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    73
  | SOME x' => tagit skolem_tag x');
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    74
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    75
fun var_or_skolem s =
24244
d7ee11ba1534 Lexicon.read_indexname/nat/variable;
wenzelm
parents: 24079
diff changeset
    76
  (case Lexicon.read_variable s of
21642
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    77
    SOME (x, i) =>
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    78
      (case try Name.dest_skolem x of
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    79
        NONE => tagit var_tag s
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    80
      | SOME x' => tagit skolem_tag
22678
23963361278c Term.string_of_vname;
wenzelm
parents: 22590
diff changeset
    81
          (setmp show_question_marks true Term.string_of_vname (x', i)))
21642
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    82
  | NONE => tagit var_tag s);
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    83
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    84
val proof_general_trans =
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    85
 Syntax.tokentrans_mode proof_generalN
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    86
  [("class", tagit class_tag),
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    87
   ("tfree", tagit tfree_tag),
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    88
   ("tvar", tagit tvar_tag),
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    89
   ("free", free_or_skolem),
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    90
   ("bound", tagit bound_tag),
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    91
   ("var", var_or_skolem)];
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    92
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    93
in
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    94
24712
64ed05609568 proper Sign operations instead of Theory aliases;
wenzelm
parents: 24555
diff changeset
    95
val _ = Context.add_setup (Sign.add_tokentrfuns proof_general_trans);
21642
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    96
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    97
end;
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    98
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
    99
23641
d6f9d3acffaa toplevel prompt/print_state: proper markup, removed hooks;
wenzelm
parents: 23621
diff changeset
   100
(* common markup *)
d6f9d3acffaa toplevel prompt/print_state: proper markup, removed hooks;
wenzelm
parents: 23621
diff changeset
   101
d6f9d3acffaa toplevel prompt/print_state: proper markup, removed hooks;
wenzelm
parents: 23621
diff changeset
   102
fun proof_general_markup (name, props) =
d6f9d3acffaa toplevel prompt/print_state: proper markup, removed hooks;
wenzelm
parents: 23621
diff changeset
   103
  (if name = Markup.promptN then ("", special "372")
23702
58ca991e0702 removed no_state markup -- produce empty state;
wenzelm
parents: 23662
diff changeset
   104
    else if name = Markup.stateN then (special "366" ^ "\n", "\n" ^ special "367")
24330
9cae2e2a4b70 Use 376/377 specials for sendback markup
aspinall
parents: 24289
diff changeset
   105
    else if name = Markup.sendbackN then (special "376", special "377")
24555
ea220faa69e7 added hilite markup;
wenzelm
parents: 24330
diff changeset
   106
    else if name = Markup.hiliteN then (special "327", special "330")
23641
d6f9d3acffaa toplevel prompt/print_state: proper markup, removed hooks;
wenzelm
parents: 23621
diff changeset
   107
    else ("", ""))
d6f9d3acffaa toplevel prompt/print_state: proper markup, removed hooks;
wenzelm
parents: 23621
diff changeset
   108
  |> (name <> Markup.promptN andalso print_mode_active "test_markup") ?
d6f9d3acffaa toplevel prompt/print_state: proper markup, removed hooks;
wenzelm
parents: 23621
diff changeset
   109
    (fn (bg, en) =>
d6f9d3acffaa toplevel prompt/print_state: proper markup, removed hooks;
wenzelm
parents: 23621
diff changeset
   110
      (bg ^ enclose "<" ">" (space_implode " " (name :: map XML.attribute props)),
d6f9d3acffaa toplevel prompt/print_state: proper markup, removed hooks;
wenzelm
parents: 23621
diff changeset
   111
        enclose "</" ">" name ^ en));
d6f9d3acffaa toplevel prompt/print_state: proper markup, removed hooks;
wenzelm
parents: 23621
diff changeset
   112
23702
58ca991e0702 removed no_state markup -- produce empty state;
wenzelm
parents: 23662
diff changeset
   113
val _ = Markup.add_mode proof_generalN proof_general_markup;
23641
d6f9d3acffaa toplevel prompt/print_state: proper markup, removed hooks;
wenzelm
parents: 23621
diff changeset
   114
d6f9d3acffaa toplevel prompt/print_state: proper markup, removed hooks;
wenzelm
parents: 23621
diff changeset
   115
21642
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   116
(* messages and notification *)
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   117
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   118
fun decorate bg en prfx =
22590
ac84debdd7d3 removed unused info channel;
wenzelm
parents: 22228
diff changeset
   119
  Output.writeln_default o enclose bg en o prefix_lines prfx;
21642
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   120
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   121
fun setup_messages () =
23662
91d06b04951f simplified writeln_fn;
wenzelm
parents: 23641
diff changeset
   122
 (Output.writeln_fn := Output.writeln_default;
22590
ac84debdd7d3 removed unused info channel;
wenzelm
parents: 22228
diff changeset
   123
  Output.priority_fn := (fn s => decorate (special "360") (special "361") "" s);
ac84debdd7d3 removed unused info channel;
wenzelm
parents: 22228
diff changeset
   124
  Output.tracing_fn := (fn s => decorate (special "360" ^ special "375") (special "361") "" s);
ac84debdd7d3 removed unused info channel;
wenzelm
parents: 22228
diff changeset
   125
  Output.debug_fn := (fn s => decorate (special "362") (special "363") "+++ " s);
ac84debdd7d3 removed unused info channel;
wenzelm
parents: 22228
diff changeset
   126
  Output.warning_fn := (fn s => decorate (special "362") (special "363") "### " s);
22699
938c1011ac94 removed unused Output.panic hook -- internal to PG wrapper;
wenzelm
parents: 22678
diff changeset
   127
  Output.error_fn := (fn s => decorate (special "364") (special "365") "*** " s));
21642
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   128
22699
938c1011ac94 removed unused Output.panic hook -- internal to PG wrapper;
wenzelm
parents: 22678
diff changeset
   129
fun panic s =
938c1011ac94 removed unused Output.panic hook -- internal to PG wrapper;
wenzelm
parents: 22678
diff changeset
   130
  (decorate (special "364") (special "365") "!!! " ("## SYSTEM EXIT ##\n" ^ s); exit 1);
21642
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   131
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   132
fun emacs_notify s = decorate (special "360") (special "361") "" s;
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   133
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   134
fun tell_clear_goals () =
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21858
diff changeset
   135
  emacs_notify "Proof General, please clear the goals buffer.";
21642
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   136
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   137
fun tell_clear_response () =
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21858
diff changeset
   138
  emacs_notify "Proof General, please clear the response buffer.";
21642
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   139
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   140
fun tell_file_loaded path =
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21858
diff changeset
   141
  emacs_notify ("Proof General, this file is loaded: " ^ quote (File.platform_path path));
21642
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   142
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   143
fun tell_file_retracted path =
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21858
diff changeset
   144
  emacs_notify ("Proof General, you can unlock the file " ^ quote (File.platform_path path));
21642
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   145
24289
bfd59eb6e24e added sendback;
wenzelm
parents: 24244
diff changeset
   146
fun sendback heading prts =
bfd59eb6e24e added sendback;
wenzelm
parents: 24244
diff changeset
   147
  Pretty.writeln (Pretty.big_list heading [Pretty.markup Markup.sendback prts]);
bfd59eb6e24e added sendback;
wenzelm
parents: 24244
diff changeset
   148
21642
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   149
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   150
(* theory loader actions *)
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   151
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   152
local
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   153
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   154
fun trace_action action name =
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   155
  if action = ThyInfo.Update then
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   156
    List.app tell_file_loaded (ThyInfo.loaded_files name)
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   157
  else if action = ThyInfo.Outdate orelse action = ThyInfo.Remove then
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   158
    List.app tell_file_retracted (ThyInfo.loaded_files name)
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   159
  else ();
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   160
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   161
in
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   162
  fun setup_thy_loader () = ThyInfo.add_hook trace_action;
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   163
  fun sync_thy_loader () = List.app (trace_action ThyInfo.Update) (ThyInfo.names ());
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   164
end;
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   165
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   166
21948
e34bc5e4e7bc removed obsolete init_pgip;
wenzelm
parents: 21945
diff changeset
   167
(* get informed about files *)
21642
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   168
25436
ca46d8a66b69 thy_name: be very liberal about file name format (workaround problem with XEmacs on cygwin);
wenzelm
parents: 25192
diff changeset
   169
val thy_name = perhaps (try (unsuffix ".thy")) o List.last o space_explode "/";
21642
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   170
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   171
val inform_file_retracted = ThyInfo.if_known_thy ThyInfo.remove_thy o thy_name;
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   172
val inform_file_processed = ThyInfo.if_known_thy ThyInfo.touch_child_thys o thy_name;
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   173
23913
fcfacb6670ed inform_file_processed: tuned msg, no state;
wenzelm
parents: 23702
diff changeset
   174
fun proper_inform_file_processed file () =
21642
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   175
  let val name = thy_name file in
23913
fcfacb6670ed inform_file_processed: tuned msg, no state;
wenzelm
parents: 23702
diff changeset
   176
    if ThyInfo.known_thy name then
21642
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   177
     (ThyInfo.touch_child_thys name;
24079
3ba5d68e076b ThyInfo.register_thy;
wenzelm
parents: 23913
diff changeset
   178
      ThyInfo.register_thy name handle ERROR msg =>
23913
fcfacb6670ed inform_file_processed: tuned msg, no state;
wenzelm
parents: 23702
diff changeset
   179
       (warning (cat_lines [msg, "Failed to register theory: " ^ quote name]);
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 21649
diff changeset
   180
        tell_file_retracted (Path.base (Path.explode file))))
21642
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   181
    else raise Toplevel.UNDEF
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   182
  end;
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   183
23913
fcfacb6670ed inform_file_processed: tuned msg, no state;
wenzelm
parents: 23702
diff changeset
   184
fun vacuous_inform_file_processed file () =
21642
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   185
 (warning ("No theory " ^ quote (thy_name file));
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 21649
diff changeset
   186
  tell_file_retracted (Path.base (Path.explode file)));
21642
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   187
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   188
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   189
(* restart top-level loop (keeps most state information) *)
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   190
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   191
val welcome = priority o Session.welcome;
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   192
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   193
fun restart () =
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21858
diff changeset
   194
 (sync_thy_loader ();
fbd068dd4d29 minor tuning;
wenzelm
parents: 21858
diff changeset
   195
  tell_clear_goals ();
fbd068dd4d29 minor tuning;
wenzelm
parents: 21858
diff changeset
   196
  tell_clear_response ();
fbd068dd4d29 minor tuning;
wenzelm
parents: 21858
diff changeset
   197
  welcome ();
fbd068dd4d29 minor tuning;
wenzelm
parents: 21858
diff changeset
   198
  raise Toplevel.RESTART);
21642
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   199
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   200
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   201
(* theorem dependency output *)
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   202
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   203
local
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   204
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   205
val spaces_quote = space_implode " " o map quote;
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   206
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   207
fun thm_deps_message (thms, deps) =
21948
e34bc5e4e7bc removed obsolete init_pgip;
wenzelm
parents: 21945
diff changeset
   208
  emacs_notify ("Proof General, theorem dependencies of " ^ thms ^ " are " ^ deps);
21642
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   209
21968
883cd697112e removed conditional combinator;
wenzelm
parents: 21959
diff changeset
   210
fun tell_thm_deps ths =
22590
ac84debdd7d3 removed unused info channel;
wenzelm
parents: 22228
diff changeset
   211
  if print_mode_active thm_depsN then
21968
883cd697112e removed conditional combinator;
wenzelm
parents: 21959
diff changeset
   212
    let
22228
7c27195a4afc proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents: 22225
diff changeset
   213
      val names = map PureThy.get_name_hint (filter PureThy.has_name_hint ths);
22225
30ab97554602 Fix tell_thm_deps to match changse in PureThy.
aspinall
parents: 22159
diff changeset
   214
      val deps = Symtab.keys (fold Proofterm.thms_of_proof'
30ab97554602 Fix tell_thm_deps to match changse in PureThy.
aspinall
parents: 22159
diff changeset
   215
				   (map Thm.proof_of ths) Symtab.empty);
21968
883cd697112e removed conditional combinator;
wenzelm
parents: 21959
diff changeset
   216
    in
883cd697112e removed conditional combinator;
wenzelm
parents: 21959
diff changeset
   217
      if null names orelse null deps then ()
883cd697112e removed conditional combinator;
wenzelm
parents: 21959
diff changeset
   218
      else thm_deps_message (spaces_quote names, spaces_quote deps)
883cd697112e removed conditional combinator;
wenzelm
parents: 21959
diff changeset
   219
    end
883cd697112e removed conditional combinator;
wenzelm
parents: 21959
diff changeset
   220
  else ();
21642
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   221
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   222
in
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   223
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   224
fun setup_present_hook () =
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   225
  Present.add_hook (fn _ => fn res => tell_thm_deps (maps #2 res));
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   226
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   227
end;
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   228
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   229
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   230
(* additional outer syntax for Isar *)
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   231
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   232
local structure P = OuterParse and K = OuterKeyword in
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   233
25192
b568f8c5d5ca made command 'undo' silent ('ProofGeneral.undo' becomes a historical relic);
wenzelm
parents: 24882
diff changeset
   234
fun undoP () = (*undo without output -- historical*)
21642
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   235
  OuterSyntax.improper_command "ProofGeneral.undo" "(internal)" K.control
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   236
    (Scan.succeed (Toplevel.no_timing o IsarCmd.undo));
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   237
24867
e5b55d7be9bb simplified interfaces for outer syntax;
wenzelm
parents: 24712
diff changeset
   238
fun restartP () =
21642
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   239
  OuterSyntax.improper_command "ProofGeneral.restart" "(internal)" K.control
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   240
    (P.opt_unit >> (Toplevel.no_timing oo K (Toplevel.imperative restart)));
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   241
24867
e5b55d7be9bb simplified interfaces for outer syntax;
wenzelm
parents: 24712
diff changeset
   242
fun kill_proofP () =
21642
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   243
  OuterSyntax.improper_command "ProofGeneral.kill_proof" "(internal)" K.control
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   244
    (Scan.succeed (Toplevel.no_timing o IsarCmd.kill_proof_notify tell_clear_goals));
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   245
24867
e5b55d7be9bb simplified interfaces for outer syntax;
wenzelm
parents: 24712
diff changeset
   246
fun inform_file_processedP () =
21642
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   247
  OuterSyntax.improper_command "ProofGeneral.inform_file_processed" "(internal)" K.control
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   248
    (P.name >> (fn file => Toplevel.no_timing o
21959
b50182aff75f inform_file_processed: Toplevel.init_empty;
wenzelm
parents: 21948
diff changeset
   249
      Toplevel.init_empty (vacuous_inform_file_processed file) o
21642
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   250
      Toplevel.kill o
21959
b50182aff75f inform_file_processed: Toplevel.init_empty;
wenzelm
parents: 21948
diff changeset
   251
      Toplevel.init_empty (proper_inform_file_processed file)));
21642
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   252
24867
e5b55d7be9bb simplified interfaces for outer syntax;
wenzelm
parents: 24712
diff changeset
   253
fun inform_file_retractedP () =
21642
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   254
  OuterSyntax.improper_command "ProofGeneral.inform_file_retracted" "(internal)" K.control
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   255
    (P.name >> (Toplevel.no_timing oo
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   256
      (fn file => Toplevel.imperative (fn () => inform_file_retracted file))));
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   257
24867
e5b55d7be9bb simplified interfaces for outer syntax;
wenzelm
parents: 24712
diff changeset
   258
fun process_pgipP () =
21642
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   259
  OuterSyntax.improper_command "ProofGeneral.process_pgip" "(internal)" K.control
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   260
    (P.text >> (Toplevel.no_timing oo
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   261
      (fn txt => Toplevel.imperative (fn () => ProofGeneralPgip.process_pgip txt))));
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   262
24867
e5b55d7be9bb simplified interfaces for outer syntax;
wenzelm
parents: 24712
diff changeset
   263
fun init_outer_syntax () = List.app (fn f => f ())
21948
e34bc5e4e7bc removed obsolete init_pgip;
wenzelm
parents: 21945
diff changeset
   264
 [undoP, restartP, kill_proofP, inform_file_processedP, inform_file_retractedP, process_pgipP];
21642
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   265
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   266
end;
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   267
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   268
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   269
(* init *)
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   270
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   271
val initialized = ref false;
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   272
22699
938c1011ac94 removed unused Output.panic hook -- internal to PG wrapper;
wenzelm
parents: 22678
diff changeset
   273
fun init false = panic "No Proof General interface support for Isabelle/classic mode."
21940
fbd068dd4d29 minor tuning;
wenzelm
parents: 21858
diff changeset
   274
  | init true =
21968
883cd697112e removed conditional combinator;
wenzelm
parents: 21959
diff changeset
   275
      (! initialized orelse
22590
ac84debdd7d3 removed unused info channel;
wenzelm
parents: 22228
diff changeset
   276
        (Output.no_warnings init_outer_syntax ();
21968
883cd697112e removed conditional combinator;
wenzelm
parents: 21959
diff changeset
   277
          setup_xsymbols_output ();
883cd697112e removed conditional combinator;
wenzelm
parents: 21959
diff changeset
   278
          setup_messages ();
22590
ac84debdd7d3 removed unused info channel;
wenzelm
parents: 22228
diff changeset
   279
          ProofGeneralPgip.init_pgip_channel (! Output.priority_fn);
21968
883cd697112e removed conditional combinator;
wenzelm
parents: 21959
diff changeset
   280
          setup_thy_loader ();
883cd697112e removed conditional combinator;
wenzelm
parents: 21959
diff changeset
   281
          setup_present_hook ();
883cd697112e removed conditional combinator;
wenzelm
parents: 21959
diff changeset
   282
          set initialized);
883cd697112e removed conditional combinator;
wenzelm
parents: 21959
diff changeset
   283
        sync_thy_loader ();
883cd697112e removed conditional combinator;
wenzelm
parents: 21959
diff changeset
   284
       change print_mode (cons proof_generalN o remove (op =) proof_generalN);
883cd697112e removed conditional combinator;
wenzelm
parents: 21959
diff changeset
   285
       Isar.sync_main ());
21642
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   286
54b00ca67e0e Add separate PG Emacs configuration
aspinall
parents:
diff changeset
   287
end;