src/Pure/ProofGeneral/proof_general_emacs.ML
author wenzelm
Fri Jun 13 21:04:42 2008 +0200 (2008-06-13)
changeset 27195 bbf4cbc69243
parent 26706 4ea64590d28b
child 27532 f3d92b5dcd45
permissions -rw-r--r--
map_const: soft version, no failure here;
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.
wenzelm@26549
     6
See also http://proofgeneral.inf.ed.ac.uk
aspinall@21642
     7
*)
aspinall@21642
     8
aspinall@21642
     9
signature PROOF_GENERAL =
aspinall@21642
    10
sig
wenzelm@26549
    11
  val test_markupN: string
aspinall@21642
    12
  val init: bool -> unit
wenzelm@24874
    13
  val init_outer_syntax: unit -> unit
wenzelm@24289
    14
  val sendback: string -> Pretty.T list -> unit
aspinall@21642
    15
end;
aspinall@21642
    16
aspinall@21642
    17
structure ProofGeneral: PROOF_GENERAL =
aspinall@21642
    18
struct
aspinall@21642
    19
wenzelm@21945
    20
aspinall@21642
    21
(* print modes *)
aspinall@21642
    22
aspinall@21642
    23
val proof_generalN = "ProofGeneralEmacs";  (*token markup (colouring vars, etc.)*)
aspinall@21642
    24
val pgasciiN = "PGASCII";                  (*plain 7-bit ASCII communication*)
aspinall@21642
    25
val thm_depsN = "thm_deps";                (*meta-information about theorem deps*)
wenzelm@26549
    26
val test_markupN = "test_markup";          (*XML markup for everything*)
wenzelm@26549
    27
wenzelm@26549
    28
val _ = Markup.add_mode test_markupN XML.output_markup;
aspinall@21642
    29
aspinall@21642
    30
fun special oct =
wenzelm@26526
    31
  if print_mode_active pgasciiN then Symbol.SOH ^ chr (ord (oct_char oct) - 167)
aspinall@21642
    32
  else oct_char oct;
aspinall@21642
    33
aspinall@21642
    34
aspinall@21642
    35
(* text output: print modes for xsymbol *)
aspinall@21642
    36
aspinall@21642
    37
local
aspinall@21642
    38
aspinall@21642
    39
fun xsym_output "\\" = "\\\\"
aspinall@21642
    40
  | xsym_output s = if Symbol.is_raw s then Symbol.decode_raw s else s;
aspinall@21642
    41
aspinall@21642
    42
fun xsymbols_output s =
wenzelm@22590
    43
  if print_mode_active Symbol.xsymbolsN andalso exists_string (equal "\\") s then
aspinall@21642
    44
    let val syms = Symbol.explode s
wenzelm@23621
    45
    in (implode (map xsym_output syms), Symbol.length syms) end
wenzelm@23621
    46
  else Output.default_output s;
aspinall@21642
    47
aspinall@21642
    48
in
aspinall@21642
    49
aspinall@21642
    50
fun setup_xsymbols_output () =
wenzelm@23641
    51
  Output.add_mode Symbol.xsymbolsN xsymbols_output Symbol.encode_raw;
aspinall@21642
    52
aspinall@21642
    53
end;
aspinall@21642
    54
aspinall@21642
    55
wenzelm@23641
    56
(* common markup *)
wenzelm@23641
    57
wenzelm@26706
    58
val _ = Markup.add_mode proof_generalN (fn (name, props) =>
wenzelm@25630
    59
  let
wenzelm@25630
    60
    val (bg1, en1) =
wenzelm@25848
    61
      if name = Markup.stateN then (special "366" ^ "\n", "\n" ^ special "367")
wenzelm@25630
    62
      else if name = Markup.sendbackN then (special "376", special "377")
wenzelm@25630
    63
      else if name = Markup.hiliteN then (special "327", special "330")
wenzelm@26706
    64
      else if name = Markup.classN then (special "351", special "350")
wenzelm@26706
    65
      else if name = Markup.tfreeN then (special "352", special "350")
wenzelm@26706
    66
      else if name = Markup.tvarN then (special "353", special "350")
wenzelm@26706
    67
      else if name = Markup.freeN then (special "354", special "350")
wenzelm@26706
    68
      else if name = Markup.boundN then (special "355", special "350")
wenzelm@26706
    69
      else if name = Markup.varN then (special "356", special "350")
wenzelm@26706
    70
      else if name = Markup.skolemN then (special "357", special "350")
wenzelm@25630
    71
      else ("", "");
wenzelm@25630
    72
    val (bg2, en2) =
wenzelm@26549
    73
      if print_mode_active test_markupN
wenzelm@26542
    74
      then XML.output_markup (name, props)
wenzelm@25630
    75
      else ("", "");
wenzelm@26706
    76
  in (bg1 ^ bg2, en2 ^ en1) end);
wenzelm@23641
    77
wenzelm@23641
    78
aspinall@21642
    79
(* messages and notification *)
aspinall@21642
    80
aspinall@21642
    81
fun decorate bg en prfx =
wenzelm@22590
    82
  Output.writeln_default o enclose bg en o prefix_lines prfx;
aspinall@21642
    83
aspinall@21642
    84
fun setup_messages () =
wenzelm@23662
    85
 (Output.writeln_fn := Output.writeln_default;
wenzelm@22590
    86
  Output.priority_fn := (fn s => decorate (special "360") (special "361") "" s);
wenzelm@22590
    87
  Output.tracing_fn := (fn s => decorate (special "360" ^ special "375") (special "361") "" s);
wenzelm@22590
    88
  Output.debug_fn := (fn s => decorate (special "362") (special "363") "+++ " s);
wenzelm@22590
    89
  Output.warning_fn := (fn s => decorate (special "362") (special "363") "### " s);
wenzelm@25848
    90
  Output.error_fn := (fn s => decorate (special "364") (special "365") "*** " s);
wenzelm@25848
    91
  Output.prompt_fn := (fn s => Output.std_output (s ^ special "372")));
aspinall@21642
    92
wenzelm@22699
    93
fun panic s =
wenzelm@22699
    94
  (decorate (special "364") (special "365") "!!! " ("## SYSTEM EXIT ##\n" ^ s); exit 1);
aspinall@21642
    95
aspinall@21642
    96
fun emacs_notify s = decorate (special "360") (special "361") "" s;
aspinall@21642
    97
aspinall@21642
    98
fun tell_clear_goals () =
wenzelm@21940
    99
  emacs_notify "Proof General, please clear the goals buffer.";
aspinall@21642
   100
aspinall@21642
   101
fun tell_clear_response () =
wenzelm@21940
   102
  emacs_notify "Proof General, please clear the response buffer.";
aspinall@21642
   103
aspinall@21642
   104
fun tell_file_loaded path =
wenzelm@21940
   105
  emacs_notify ("Proof General, this file is loaded: " ^ quote (File.platform_path path));
aspinall@21642
   106
aspinall@21642
   107
fun tell_file_retracted path =
wenzelm@21940
   108
  emacs_notify ("Proof General, you can unlock the file " ^ quote (File.platform_path path));
aspinall@21642
   109
wenzelm@24289
   110
fun sendback heading prts =
wenzelm@24289
   111
  Pretty.writeln (Pretty.big_list heading [Pretty.markup Markup.sendback prts]);
wenzelm@24289
   112
aspinall@21642
   113
aspinall@21642
   114
(* theory loader actions *)
aspinall@21642
   115
aspinall@21642
   116
local
aspinall@21642
   117
aspinall@21642
   118
fun trace_action action name =
aspinall@21642
   119
  if action = ThyInfo.Update then
aspinall@21642
   120
    List.app tell_file_loaded (ThyInfo.loaded_files name)
aspinall@21642
   121
  else if action = ThyInfo.Outdate orelse action = ThyInfo.Remove then
aspinall@21642
   122
    List.app tell_file_retracted (ThyInfo.loaded_files name)
aspinall@21642
   123
  else ();
aspinall@21642
   124
aspinall@21642
   125
in
aspinall@21642
   126
  fun setup_thy_loader () = ThyInfo.add_hook trace_action;
wenzelm@26613
   127
  fun sync_thy_loader () = List.app (trace_action ThyInfo.Update) (ThyInfo.get_names ());
aspinall@21642
   128
end;
aspinall@21642
   129
aspinall@21642
   130
wenzelm@21948
   131
(* get informed about files *)
aspinall@21642
   132
wenzelm@25442
   133
local
aspinall@21642
   134
wenzelm@25442
   135
(*liberal low-level version*)
wenzelm@25442
   136
val thy_name = perhaps (try (unsuffix ".thy")) o List.last o space_explode "/";
wenzelm@25442
   137
val thy_path = ThyLoad.thy_path o thy_name;
wenzelm@25442
   138
wenzelm@25442
   139
in
wenzelm@25442
   140
wenzelm@25443
   141
fun check_thy "" = false
wenzelm@25443
   142
  | check_thy file = ThyInfo.check_known_thy (thy_name file);
aspinall@21642
   143
wenzelm@23913
   144
fun proper_inform_file_processed file () =
wenzelm@25442
   145
  let
wenzelm@25442
   146
    val name = thy_name file;
wenzelm@25442
   147
    val _ = ThyInfo.touch_child_thys name;
wenzelm@25442
   148
    val _ = ThyInfo.register_thy name handle ERROR msg =>
wenzelm@25442
   149
      (warning (cat_lines [msg, "Failed to register theory: " ^ quote name]);
wenzelm@25442
   150
        tell_file_retracted (thy_path file));
wenzelm@25442
   151
  in () end;
aspinall@21642
   152
wenzelm@25442
   153
fun vacuous_inform_file_processed file () = tell_file_retracted (thy_path file);
wenzelm@25442
   154
wenzelm@25442
   155
val inform_file_retracted = ThyInfo.if_known_thy ThyInfo.remove_thy o thy_name;
wenzelm@25442
   156
wenzelm@25442
   157
end;
aspinall@21642
   158
aspinall@21642
   159
aspinall@21642
   160
(* restart top-level loop (keeps most state information) *)
aspinall@21642
   161
aspinall@21642
   162
val welcome = priority o Session.welcome;
aspinall@21642
   163
aspinall@21642
   164
fun restart () =
wenzelm@21940
   165
 (sync_thy_loader ();
wenzelm@21940
   166
  tell_clear_goals ();
wenzelm@21940
   167
  tell_clear_response ();
wenzelm@21940
   168
  welcome ();
wenzelm@21940
   169
  raise Toplevel.RESTART);
aspinall@21642
   170
aspinall@21642
   171
aspinall@21642
   172
(* theorem dependency output *)
aspinall@21642
   173
aspinall@21642
   174
local
aspinall@21642
   175
aspinall@21642
   176
val spaces_quote = space_implode " " o map quote;
aspinall@21642
   177
aspinall@21642
   178
fun thm_deps_message (thms, deps) =
wenzelm@21948
   179
  emacs_notify ("Proof General, theorem dependencies of " ^ thms ^ " are " ^ deps);
aspinall@21642
   180
wenzelm@21968
   181
fun tell_thm_deps ths =
wenzelm@22590
   182
  if print_mode_active thm_depsN then
wenzelm@21968
   183
    let
wenzelm@22228
   184
      val names = map PureThy.get_name_hint (filter PureThy.has_name_hint ths);
aspinall@22225
   185
      val deps = Symtab.keys (fold Proofterm.thms_of_proof'
aspinall@22225
   186
				   (map Thm.proof_of ths) Symtab.empty);
wenzelm@21968
   187
    in
wenzelm@21968
   188
      if null names orelse null deps then ()
wenzelm@21968
   189
      else thm_deps_message (spaces_quote names, spaces_quote deps)
wenzelm@21968
   190
    end
wenzelm@21968
   191
  else ();
aspinall@21642
   192
aspinall@21642
   193
in
aspinall@21642
   194
aspinall@21642
   195
fun setup_present_hook () =
aspinall@21642
   196
  Present.add_hook (fn _ => fn res => tell_thm_deps (maps #2 res));
aspinall@21642
   197
aspinall@21642
   198
end;
aspinall@21642
   199
aspinall@21642
   200
aspinall@21642
   201
(* additional outer syntax for Isar *)
aspinall@21642
   202
aspinall@21642
   203
local structure P = OuterParse and K = OuterKeyword in
aspinall@21642
   204
wenzelm@25192
   205
fun undoP () = (*undo without output -- historical*)
aspinall@21642
   206
  OuterSyntax.improper_command "ProofGeneral.undo" "(internal)" K.control
aspinall@21642
   207
    (Scan.succeed (Toplevel.no_timing o IsarCmd.undo));
aspinall@21642
   208
wenzelm@24867
   209
fun restartP () =
aspinall@21642
   210
  OuterSyntax.improper_command "ProofGeneral.restart" "(internal)" K.control
aspinall@21642
   211
    (P.opt_unit >> (Toplevel.no_timing oo K (Toplevel.imperative restart)));
aspinall@21642
   212
wenzelm@24867
   213
fun kill_proofP () =
aspinall@21642
   214
  OuterSyntax.improper_command "ProofGeneral.kill_proof" "(internal)" K.control
aspinall@21642
   215
    (Scan.succeed (Toplevel.no_timing o IsarCmd.kill_proof_notify tell_clear_goals));
aspinall@21642
   216
wenzelm@24867
   217
fun inform_file_processedP () =
aspinall@21642
   218
  OuterSyntax.improper_command "ProofGeneral.inform_file_processed" "(internal)" K.control
aspinall@21642
   219
    (P.name >> (fn file => Toplevel.no_timing o
wenzelm@25443
   220
      Toplevel.imperative (fn () => error "Bad file name") o
wenzelm@25443
   221
      Toplevel.init_empty (fn _ => file <> "") (vacuous_inform_file_processed file) o
aspinall@21642
   222
      Toplevel.kill o
wenzelm@25442
   223
      Toplevel.init_empty (fn _ => check_thy file) (proper_inform_file_processed file)));
aspinall@21642
   224
wenzelm@24867
   225
fun inform_file_retractedP () =
aspinall@21642
   226
  OuterSyntax.improper_command "ProofGeneral.inform_file_retracted" "(internal)" K.control
aspinall@21642
   227
    (P.name >> (Toplevel.no_timing oo
aspinall@21642
   228
      (fn file => Toplevel.imperative (fn () => inform_file_retracted file))));
aspinall@21642
   229
wenzelm@24867
   230
fun process_pgipP () =
aspinall@21642
   231
  OuterSyntax.improper_command "ProofGeneral.process_pgip" "(internal)" K.control
aspinall@21642
   232
    (P.text >> (Toplevel.no_timing oo
aspinall@21642
   233
      (fn txt => Toplevel.imperative (fn () => ProofGeneralPgip.process_pgip txt))));
aspinall@21642
   234
wenzelm@24867
   235
fun init_outer_syntax () = List.app (fn f => f ())
wenzelm@21948
   236
 [undoP, restartP, kill_proofP, inform_file_processedP, inform_file_retractedP, process_pgipP];
aspinall@21642
   237
aspinall@21642
   238
end;
aspinall@21642
   239
aspinall@21642
   240
aspinall@21642
   241
(* init *)
aspinall@21642
   242
aspinall@21642
   243
val initialized = ref false;
aspinall@21642
   244
wenzelm@22699
   245
fun init false = panic "No Proof General interface support for Isabelle/classic mode."
wenzelm@21940
   246
  | init true =
wenzelm@21968
   247
      (! initialized orelse
wenzelm@22590
   248
        (Output.no_warnings init_outer_syntax ();
wenzelm@21968
   249
          setup_xsymbols_output ();
wenzelm@21968
   250
          setup_messages ();
wenzelm@22590
   251
          ProofGeneralPgip.init_pgip_channel (! Output.priority_fn);
wenzelm@21968
   252
          setup_thy_loader ();
wenzelm@21968
   253
          setup_present_hook ();
wenzelm@21968
   254
          set initialized);
wenzelm@21968
   255
        sync_thy_loader ();
wenzelm@25749
   256
       change print_mode (update (op =) proof_generalN);
wenzelm@26643
   257
       Isar.toplevel_loop {init = true, welcome = true, sync = true, secure = Secure.is_secure ()});
aspinall@21642
   258
aspinall@21642
   259
end;