src/Pure/ProofGeneral/proof_general_emacs.ML
author wenzelm
Sat Oct 06 16:50:04 2007 +0200 (2007-10-06)
changeset 24867 e5b55d7be9bb
parent 24712 64ed05609568
child 24873 9de439f51e3c
permissions -rw-r--r--
simplified interfaces for outer syntax;
aspinall@21642
     1
(*  Title:      Pure/ProofGeneral/proof_general_emacs.ML
aspinall@21642
     2
    ID:         $Id$
aspinall@21642
     3
    Author:     David Aspinall and Markus Wenzel
aspinall@21642
     4
aspinall@21642
     5
Isabelle/Isar configuration for Emacs Proof General.
aspinall@21642
     6
See http://proofgeneral.inf.ed.ac.uk
aspinall@21642
     7
*)
aspinall@21642
     8
aspinall@21642
     9
signature PROOF_GENERAL =
aspinall@21642
    10
sig
aspinall@21642
    11
  val init: bool -> unit
wenzelm@24289
    12
  val sendback: string -> Pretty.T list -> unit
aspinall@21642
    13
  val write_keywords: string -> unit
aspinall@21642
    14
end;
aspinall@21642
    15
aspinall@21642
    16
structure ProofGeneral: PROOF_GENERAL =
aspinall@21642
    17
struct
aspinall@21642
    18
wenzelm@21945
    19
aspinall@21642
    20
(* print modes *)
aspinall@21642
    21
aspinall@21642
    22
val proof_generalN = "ProofGeneralEmacs";  (*token markup (colouring vars, etc.)*)
aspinall@21642
    23
val pgasciiN = "PGASCII";                  (*plain 7-bit ASCII communication*)
aspinall@21642
    24
val thm_depsN = "thm_deps";                (*meta-information about theorem deps*)
aspinall@21642
    25
aspinall@21642
    26
fun special oct =
wenzelm@22590
    27
  if print_mode_active pgasciiN then chr 1 ^ chr (ord (oct_char oct) - 167)
aspinall@21642
    28
  else oct_char oct;
aspinall@21642
    29
aspinall@21642
    30
aspinall@21642
    31
(* text output: print modes for xsymbol *)
aspinall@21642
    32
aspinall@21642
    33
local
aspinall@21642
    34
aspinall@21642
    35
fun xsym_output "\\" = "\\\\"
aspinall@21642
    36
  | xsym_output s = if Symbol.is_raw s then Symbol.decode_raw s else s;
aspinall@21642
    37
aspinall@21642
    38
fun xsymbols_output s =
wenzelm@22590
    39
  if print_mode_active Symbol.xsymbolsN andalso exists_string (equal "\\") s then
aspinall@21642
    40
    let val syms = Symbol.explode s
wenzelm@23621
    41
    in (implode (map xsym_output syms), Symbol.length syms) end
wenzelm@23621
    42
  else Output.default_output s;
aspinall@21642
    43
aspinall@21642
    44
in
aspinall@21642
    45
aspinall@21642
    46
fun setup_xsymbols_output () =
wenzelm@23641
    47
  Output.add_mode Symbol.xsymbolsN xsymbols_output Symbol.encode_raw;
aspinall@21642
    48
aspinall@21642
    49
end;
aspinall@21642
    50
aspinall@21642
    51
aspinall@21642
    52
(* token translations *)
aspinall@21642
    53
aspinall@21642
    54
local
aspinall@21642
    55
aspinall@21642
    56
fun end_tag () = special "350";
aspinall@21642
    57
val class_tag = ("class", fn () => special "351");
aspinall@21642
    58
val tfree_tag = ("tfree", fn () => special "352");
aspinall@21642
    59
val tvar_tag = ("tvar", fn () => special "353");
aspinall@21642
    60
val free_tag = ("free", fn () => special "354");
aspinall@21642
    61
val bound_tag = ("bound", fn () => special "355");
aspinall@21642
    62
val var_tag = ("var", fn () => special "356");
aspinall@21642
    63
val skolem_tag = ("skolem", fn () => special "357");
aspinall@21642
    64
aspinall@21642
    65
fun xml_atom kind x = XML.element "atom" [("kind", kind)] [XML.text x];
aspinall@21642
    66
aspinall@21642
    67
fun tagit (kind, bg_tag) x =
wenzelm@23621
    68
  (bg_tag () ^ x ^ end_tag (), Symbol.length (Symbol.explode x));
aspinall@21642
    69
aspinall@21642
    70
fun free_or_skolem x =
aspinall@21642
    71
  (case try Name.dest_skolem x of
aspinall@21642
    72
    NONE => tagit free_tag x
aspinall@21642
    73
  | SOME x' => tagit skolem_tag x');
aspinall@21642
    74
aspinall@21642
    75
fun var_or_skolem s =
wenzelm@24244
    76
  (case Lexicon.read_variable s of
aspinall@21642
    77
    SOME (x, i) =>
aspinall@21642
    78
      (case try Name.dest_skolem x of
aspinall@21642
    79
        NONE => tagit var_tag s
aspinall@21642
    80
      | SOME x' => tagit skolem_tag
wenzelm@22678
    81
          (setmp show_question_marks true Term.string_of_vname (x', i)))
aspinall@21642
    82
  | NONE => tagit var_tag s);
aspinall@21642
    83
aspinall@21642
    84
val proof_general_trans =
aspinall@21642
    85
 Syntax.tokentrans_mode proof_generalN
aspinall@21642
    86
  [("class", tagit class_tag),
aspinall@21642
    87
   ("tfree", tagit tfree_tag),
aspinall@21642
    88
   ("tvar", tagit tvar_tag),
aspinall@21642
    89
   ("free", free_or_skolem),
aspinall@21642
    90
   ("bound", tagit bound_tag),
aspinall@21642
    91
   ("var", var_or_skolem)];
aspinall@21642
    92
aspinall@21642
    93
in
aspinall@21642
    94
wenzelm@24712
    95
val _ = Context.add_setup (Sign.add_tokentrfuns proof_general_trans);
aspinall@21642
    96
aspinall@21642
    97
end;
aspinall@21642
    98
aspinall@21642
    99
wenzelm@23641
   100
(* common markup *)
wenzelm@23641
   101
wenzelm@23641
   102
fun proof_general_markup (name, props) =
wenzelm@23641
   103
  (if name = Markup.promptN then ("", special "372")
wenzelm@23702
   104
    else if name = Markup.stateN then (special "366" ^ "\n", "\n" ^ special "367")
aspinall@24330
   105
    else if name = Markup.sendbackN then (special "376", special "377")
wenzelm@24555
   106
    else if name = Markup.hiliteN then (special "327", special "330")
wenzelm@23641
   107
    else ("", ""))
wenzelm@23641
   108
  |> (name <> Markup.promptN andalso print_mode_active "test_markup") ?
wenzelm@23641
   109
    (fn (bg, en) =>
wenzelm@23641
   110
      (bg ^ enclose "<" ">" (space_implode " " (name :: map XML.attribute props)),
wenzelm@23641
   111
        enclose "</" ">" name ^ en));
wenzelm@23641
   112
wenzelm@23702
   113
val _ = Markup.add_mode proof_generalN proof_general_markup;
wenzelm@23641
   114
wenzelm@23641
   115
aspinall@21642
   116
(* messages and notification *)
aspinall@21642
   117
aspinall@21642
   118
fun decorate bg en prfx =
wenzelm@22590
   119
  Output.writeln_default o enclose bg en o prefix_lines prfx;
aspinall@21642
   120
aspinall@21642
   121
fun setup_messages () =
wenzelm@23662
   122
 (Output.writeln_fn := Output.writeln_default;
wenzelm@22590
   123
  Output.priority_fn := (fn s => decorate (special "360") (special "361") "" s);
wenzelm@22590
   124
  Output.tracing_fn := (fn s => decorate (special "360" ^ special "375") (special "361") "" s);
wenzelm@22590
   125
  Output.debug_fn := (fn s => decorate (special "362") (special "363") "+++ " s);
wenzelm@22590
   126
  Output.warning_fn := (fn s => decorate (special "362") (special "363") "### " s);
wenzelm@22699
   127
  Output.error_fn := (fn s => decorate (special "364") (special "365") "*** " s));
aspinall@21642
   128
wenzelm@22699
   129
fun panic s =
wenzelm@22699
   130
  (decorate (special "364") (special "365") "!!! " ("## SYSTEM EXIT ##\n" ^ s); exit 1);
aspinall@21642
   131
aspinall@21642
   132
fun emacs_notify s = decorate (special "360") (special "361") "" s;
aspinall@21642
   133
aspinall@21642
   134
fun tell_clear_goals () =
wenzelm@21940
   135
  emacs_notify "Proof General, please clear the goals buffer.";
aspinall@21642
   136
aspinall@21642
   137
fun tell_clear_response () =
wenzelm@21940
   138
  emacs_notify "Proof General, please clear the response buffer.";
aspinall@21642
   139
aspinall@21642
   140
fun tell_file_loaded path =
wenzelm@21940
   141
  emacs_notify ("Proof General, this file is loaded: " ^ quote (File.platform_path path));
aspinall@21642
   142
aspinall@21642
   143
fun tell_file_retracted path =
wenzelm@21940
   144
  emacs_notify ("Proof General, you can unlock the file " ^ quote (File.platform_path path));
aspinall@21642
   145
wenzelm@24289
   146
fun sendback heading prts =
wenzelm@24289
   147
  Pretty.writeln (Pretty.big_list heading [Pretty.markup Markup.sendback prts]);
wenzelm@24289
   148
aspinall@21642
   149
aspinall@21642
   150
(* theory loader actions *)
aspinall@21642
   151
aspinall@21642
   152
local
aspinall@21642
   153
aspinall@21642
   154
fun trace_action action name =
aspinall@21642
   155
  if action = ThyInfo.Update then
aspinall@21642
   156
    List.app tell_file_loaded (ThyInfo.loaded_files name)
aspinall@21642
   157
  else if action = ThyInfo.Outdate orelse action = ThyInfo.Remove then
aspinall@21642
   158
    List.app tell_file_retracted (ThyInfo.loaded_files name)
aspinall@21642
   159
  else ();
aspinall@21642
   160
aspinall@21642
   161
in
aspinall@21642
   162
  fun setup_thy_loader () = ThyInfo.add_hook trace_action;
aspinall@21642
   163
  fun sync_thy_loader () = List.app (trace_action ThyInfo.Update) (ThyInfo.names ());
aspinall@21642
   164
end;
aspinall@21642
   165
aspinall@21642
   166
wenzelm@21948
   167
(* get informed about files *)
aspinall@21642
   168
wenzelm@21858
   169
val thy_name = Path.implode o #1 o Path.split_ext o Path.base o Path.explode;
aspinall@21642
   170
aspinall@21642
   171
val inform_file_retracted = ThyInfo.if_known_thy ThyInfo.remove_thy o thy_name;
aspinall@21642
   172
val inform_file_processed = ThyInfo.if_known_thy ThyInfo.touch_child_thys o thy_name;
aspinall@21642
   173
wenzelm@23913
   174
fun proper_inform_file_processed file () =
aspinall@21642
   175
  let val name = thy_name file in
wenzelm@23913
   176
    if ThyInfo.known_thy name then
aspinall@21642
   177
     (ThyInfo.touch_child_thys name;
wenzelm@24079
   178
      ThyInfo.register_thy name handle ERROR msg =>
wenzelm@23913
   179
       (warning (cat_lines [msg, "Failed to register theory: " ^ quote name]);
wenzelm@21858
   180
        tell_file_retracted (Path.base (Path.explode file))))
aspinall@21642
   181
    else raise Toplevel.UNDEF
aspinall@21642
   182
  end;
aspinall@21642
   183
wenzelm@23913
   184
fun vacuous_inform_file_processed file () =
aspinall@21642
   185
 (warning ("No theory " ^ quote (thy_name file));
wenzelm@21858
   186
  tell_file_retracted (Path.base (Path.explode file)));
aspinall@21642
   187
aspinall@21642
   188
aspinall@21642
   189
(* restart top-level loop (keeps most state information) *)
aspinall@21642
   190
aspinall@21642
   191
val welcome = priority o Session.welcome;
aspinall@21642
   192
aspinall@21642
   193
fun restart () =
wenzelm@21940
   194
 (sync_thy_loader ();
wenzelm@21940
   195
  tell_clear_goals ();
wenzelm@21940
   196
  tell_clear_response ();
wenzelm@21940
   197
  welcome ();
wenzelm@21940
   198
  raise Toplevel.RESTART);
aspinall@21642
   199
aspinall@21642
   200
aspinall@21642
   201
(* theorem dependency output *)
aspinall@21642
   202
aspinall@21642
   203
local
aspinall@21642
   204
aspinall@21642
   205
val spaces_quote = space_implode " " o map quote;
aspinall@21642
   206
aspinall@21642
   207
fun thm_deps_message (thms, deps) =
wenzelm@21948
   208
  emacs_notify ("Proof General, theorem dependencies of " ^ thms ^ " are " ^ deps);
aspinall@21642
   209
wenzelm@21968
   210
fun tell_thm_deps ths =
wenzelm@22590
   211
  if print_mode_active thm_depsN then
wenzelm@21968
   212
    let
wenzelm@22228
   213
      val names = map PureThy.get_name_hint (filter PureThy.has_name_hint ths);
aspinall@22225
   214
      val deps = Symtab.keys (fold Proofterm.thms_of_proof'
aspinall@22225
   215
				   (map Thm.proof_of ths) Symtab.empty);
wenzelm@21968
   216
    in
wenzelm@21968
   217
      if null names orelse null deps then ()
wenzelm@21968
   218
      else thm_deps_message (spaces_quote names, spaces_quote deps)
wenzelm@21968
   219
    end
wenzelm@21968
   220
  else ();
aspinall@21642
   221
aspinall@21642
   222
in
aspinall@21642
   223
aspinall@21642
   224
fun setup_present_hook () =
aspinall@21642
   225
  Present.add_hook (fn _ => fn res => tell_thm_deps (maps #2 res));
aspinall@21642
   226
aspinall@21642
   227
end;
aspinall@21642
   228
aspinall@21642
   229
aspinall@21642
   230
(* additional outer syntax for Isar *)
aspinall@21642
   231
aspinall@21642
   232
local structure P = OuterParse and K = OuterKeyword in
aspinall@21642
   233
wenzelm@24867
   234
fun undoP () = (*undo without output*)
aspinall@21642
   235
  OuterSyntax.improper_command "ProofGeneral.undo" "(internal)" K.control
aspinall@21642
   236
    (Scan.succeed (Toplevel.no_timing o IsarCmd.undo));
aspinall@21642
   237
wenzelm@24867
   238
fun restartP () =
aspinall@21642
   239
  OuterSyntax.improper_command "ProofGeneral.restart" "(internal)" K.control
aspinall@21642
   240
    (P.opt_unit >> (Toplevel.no_timing oo K (Toplevel.imperative restart)));
aspinall@21642
   241
wenzelm@24867
   242
fun kill_proofP () =
aspinall@21642
   243
  OuterSyntax.improper_command "ProofGeneral.kill_proof" "(internal)" K.control
aspinall@21642
   244
    (Scan.succeed (Toplevel.no_timing o IsarCmd.kill_proof_notify tell_clear_goals));
aspinall@21642
   245
wenzelm@24867
   246
fun inform_file_processedP () =
aspinall@21642
   247
  OuterSyntax.improper_command "ProofGeneral.inform_file_processed" "(internal)" K.control
aspinall@21642
   248
    (P.name >> (fn file => Toplevel.no_timing o
wenzelm@21959
   249
      Toplevel.init_empty (vacuous_inform_file_processed file) o
aspinall@21642
   250
      Toplevel.kill o
wenzelm@21959
   251
      Toplevel.init_empty (proper_inform_file_processed file)));
aspinall@21642
   252
wenzelm@24867
   253
fun inform_file_retractedP () =
aspinall@21642
   254
  OuterSyntax.improper_command "ProofGeneral.inform_file_retracted" "(internal)" K.control
aspinall@21642
   255
    (P.name >> (Toplevel.no_timing oo
aspinall@21642
   256
      (fn file => Toplevel.imperative (fn () => inform_file_retracted file))));
aspinall@21642
   257
wenzelm@24867
   258
fun process_pgipP () =
aspinall@21642
   259
  OuterSyntax.improper_command "ProofGeneral.process_pgip" "(internal)" K.control
aspinall@21642
   260
    (P.text >> (Toplevel.no_timing oo
aspinall@21642
   261
      (fn txt => Toplevel.imperative (fn () => ProofGeneralPgip.process_pgip txt))));
aspinall@21642
   262
wenzelm@24867
   263
fun init_outer_syntax () = List.app (fn f => f ())
wenzelm@21948
   264
 [undoP, restartP, kill_proofP, inform_file_processedP, inform_file_retractedP, process_pgipP];
aspinall@21642
   265
aspinall@21642
   266
end;
aspinall@21642
   267
aspinall@21642
   268
aspinall@21642
   269
(* init *)
aspinall@21642
   270
aspinall@21642
   271
val initialized = ref false;
aspinall@21642
   272
wenzelm@22699
   273
fun init false = panic "No Proof General interface support for Isabelle/classic mode."
wenzelm@21940
   274
  | init true =
wenzelm@21968
   275
      (! initialized orelse
wenzelm@22590
   276
        (Output.no_warnings init_outer_syntax ();
wenzelm@21968
   277
          setup_xsymbols_output ();
wenzelm@21968
   278
          setup_messages ();
wenzelm@22590
   279
          ProofGeneralPgip.init_pgip_channel (! Output.priority_fn);
wenzelm@21968
   280
          setup_thy_loader ();
wenzelm@21968
   281
          setup_present_hook ();
wenzelm@21968
   282
          set initialized);
wenzelm@21968
   283
        sync_thy_loader ();
wenzelm@21968
   284
       change print_mode (cons proof_generalN o remove (op =) proof_generalN);
wenzelm@21968
   285
       Isar.sync_main ());
aspinall@21642
   286
aspinall@21642
   287
aspinall@21642
   288
wenzelm@21968
   289
 (** generate elisp file for keyword classification **)
aspinall@21642
   290
aspinall@21642
   291
local
aspinall@21642
   292
aspinall@21642
   293
val regexp_meta = member (op =) (explode ".*+?[]^$");
wenzelm@21940
   294
val regexp_quote = translate_string (fn c => if regexp_meta c then "\\\\" ^ c else c);
aspinall@21642
   295
aspinall@21642
   296
fun defconst name strs =
aspinall@21642
   297
  "\n(defconst isar-keywords-" ^ name ^
aspinall@21642
   298
  "\n  '(" ^ space_implode "\n    " (map (quote o regexp_quote) strs) ^ "))\n";
aspinall@21642
   299
aspinall@21642
   300
fun make_elisp_commands commands kind = defconst kind
aspinall@21642
   301
  (commands |> map_filter (fn (c, _, k, _) => if k = kind then SOME c else NONE));
aspinall@21642
   302
aspinall@21642
   303
fun make_elisp_syntax (keywords, commands) =
aspinall@21642
   304
  ";;\n\
aspinall@21642
   305
  \;; Keyword classification tables for Isabelle/Isar.\n\
aspinall@21642
   306
  \;; This file was generated by " ^ Session.name () ^ " -- DO NOT EDIT!\n\
aspinall@21642
   307
  \;;\n\
aspinall@21642
   308
  \;; $" ^ "Id$\n\
aspinall@21642
   309
  \;;\n" ^
aspinall@21642
   310
  defconst "major" (map #1 commands) ^
wenzelm@21940
   311
  defconst "minor" (filter Syntax.is_identifier keywords) ^
aspinall@21642
   312
  implode (map (make_elisp_commands commands) OuterKeyword.kinds) ^
aspinall@21642
   313
  "\n(provide 'isar-keywords)\n";
aspinall@21642
   314
aspinall@21642
   315
in
aspinall@21642
   316
aspinall@21642
   317
fun write_keywords s =
aspinall@21642
   318
 (init_outer_syntax ();
wenzelm@21858
   319
  File.write (Path.explode ("isar-keywords" ^ (if s = "" then "" else "-" ^ s) ^".el"))
aspinall@21642
   320
    (make_elisp_syntax (OuterSyntax.dest_keywords (), OuterSyntax.dest_parsers ())));
aspinall@21642
   321
aspinall@21642
   322
end;
aspinall@21642
   323
aspinall@21642
   324
end;