src/Pure/proof_general.ML
author wenzelm
Tue Nov 28 00:35:21 2006 +0100 (2006-11-28)
changeset 21566 af2932baf068
parent 21562 dd39c9e62f19
child 21631 2cc00b360b2c
permissions -rw-r--r--
dest_term: strip_imp_concl;
wenzelm@12780
     1
(*  Title:      Pure/proof_general.ML
wenzelm@12778
     2
    ID:         $Id$
wenzelm@14675
     3
    Author:     David Aspinall and Markus Wenzel
wenzelm@12778
     4
wenzelm@17469
     5
Isabelle configuration for Proof General (see
wenzelm@17469
     6
http://proofgeneral.inf.ed.ac.uk).  Also includes experimental support
wenzelm@17469
     7
for PGIP control language for Isabelle/Isar (PGIP 2.X).
wenzelm@12778
     8
*)
wenzelm@12778
     9
wenzelm@12778
    10
signature PROOF_GENERAL =
wenzelm@12778
    11
sig
wenzelm@12778
    12
  val update_thy_only: string -> unit
wenzelm@12778
    13
  val try_update_thy_only: string -> unit
wenzelm@13391
    14
  val inform_file_retracted: string -> unit
wenzelm@12778
    15
  val inform_file_processed: string -> unit
wenzelm@16534
    16
  val preferences:
wenzelm@16534
    17
      (string *
wenzelm@16534
    18
        (string *
wenzelm@16534
    19
         (string *
wenzelm@16534
    20
          (string * (string * (unit -> string)) *
wenzelm@16534
    21
           (string -> unit)))) list) list ref
berghofe@13728
    22
  val process_pgip: string -> unit
wenzelm@12778
    23
  val thms_containing: string list -> unit
wenzelm@12778
    24
  val help: unit -> unit
wenzelm@12778
    25
  val show_context: unit -> theory
wenzelm@12778
    26
  val kill_goal: unit -> unit
wenzelm@12778
    27
  val repeat_undo: int -> unit
wenzelm@12778
    28
  val isa_restart: unit -> unit
wenzelm@12833
    29
  val full_proofs: bool -> unit
aspinall@15134
    30
  val isarcmd: string -> unit
wenzelm@12778
    31
  val init: bool -> unit
aspinall@15134
    32
  val init_pgip: bool -> unit
wenzelm@12778
    33
  val write_keywords: string -> unit
wenzelm@16534
    34
  val xmls_of_str: string -> string list   (*temp for testing parser*)
wenzelm@12778
    35
end;
wenzelm@12778
    36
wenzelm@16534
    37
structure ProofGeneral: PROOF_GENERAL =
wenzelm@12778
    38
struct
wenzelm@12778
    39
wenzelm@16534
    40
structure P = OuterParse;
aspinall@15145
    41
aspinall@15191
    42
aspinall@15134
    43
(* PGIP messaging mode (independent of PGML output) *)
aspinall@15134
    44
aspinall@15134
    45
val pgip_active = ref false;
aspinall@15134
    46
val pgip_emacs_compatibility_flag = ref false;
aspinall@15134
    47
wenzelm@16534
    48
fun pgip () = (! pgip_active);
wenzelm@16534
    49
fun pgip_emacs_compatibility () = (! pgip_emacs_compatibility_flag);
aspinall@15134
    50
aspinall@15134
    51
wenzelm@12778
    52
(* print modes *)
wenzelm@12778
    53
wenzelm@16534
    54
val proof_generalN = "ProofGeneral";  (*token markup (colouring vars, etc.)*)
wenzelm@17217
    55
val pgasciiN = "PGASCII";             (*plain 7-bit ASCII communication*)
wenzelm@16534
    56
val xsymbolsN = Symbol.xsymbolsN;     (*X-Symbol symbols*)
wenzelm@16534
    57
val pgmlN = "PGML";                   (*XML escapes and PGML symbol elements*)
wenzelm@16534
    58
val pgmlatomsN = "PGMLatoms";         (*variable kind decorations*)
wenzelm@16534
    59
val thm_depsN = "thm_deps";           (*meta-information about theorem deps*)
wenzelm@12778
    60
wenzelm@16534
    61
fun pgml () = Output.has_mode pgmlN;
wenzelm@16534
    62
wenzelm@17217
    63
fun special oct =
wenzelm@17217
    64
  if Output.has_mode pgasciiN then chr 1 ^ chr (ord (oct_char oct) - 167)
wenzelm@17217
    65
  else oct_char oct;
wenzelm@17217
    66
wenzelm@12778
    67
aspinall@15134
    68
(* text output: print modes for xsymbol and PGML *)
wenzelm@12778
    69
wenzelm@12778
    70
local
wenzelm@12778
    71
wenzelm@14827
    72
fun xsym_output "\\" = "\\\\"
wenzelm@14827
    73
  | xsym_output s = if Symbol.is_raw s then Symbol.decode_raw s else s;
wenzelm@14827
    74
wenzelm@12778
    75
fun xsymbols_output s =
wenzelm@16534
    76
  if Output.has_mode xsymbolsN andalso exists_string (equal "\\") s then
wenzelm@12778
    77
    let val syms = Symbol.explode s
wenzelm@14827
    78
    in (implode (map xsym_output syms), real (Symbol.length syms)) end
aspinall@15134
    79
  else Symbol.default_output s;
aspinall@15134
    80
aspinall@15134
    81
fun pgml_sym s =
aspinall@15134
    82
  (case Symbol.decode s of
wenzelm@16534
    83
    (*NB: an alternative here would be to output the default print mode alternative
wenzelm@16534
    84
      in the element content, but unfortunately print modes are not that fine grained.*)
aspinall@15266
    85
    Symbol.Char s => XML.text s
aspinall@15403
    86
  | Symbol.Sym sn => XML.element "sym" [("name", sn)] [XML.text s]
wenzelm@16534
    87
  | Symbol.Ctrl sn => XML.element "ctrl" [("name", sn)] [XML.text s] (* FIXME: no such PGML! *)
aspinall@15266
    88
  | Symbol.Raw s => s);
wenzelm@12778
    89
aspinall@15134
    90
fun pgml_output str =
aspinall@15134
    91
  let val syms = Symbol.explode str
aspinall@15134
    92
  in (implode (map pgml_sym syms), real (Symbol.length syms)) end;
aspinall@15134
    93
wenzelm@16534
    94
in
wenzelm@12778
    95
wenzelm@16534
    96
fun setup_xsymbols_output () =
wenzelm@16534
    97
  Output.add_mode xsymbolsN
wenzelm@19265
    98
    (xsymbols_output, K xsymbols_output, Symbol.default_indent, Symbol.encode_raw);
wenzelm@12778
    99
wenzelm@16534
   100
fun setup_pgml_output () =
wenzelm@16534
   101
  Output.add_mode pgmlN
wenzelm@19265
   102
    (pgml_output, K pgml_output, Symbol.default_indent, Symbol.encode_raw);
wenzelm@12778
   103
wenzelm@12778
   104
end;
wenzelm@12778
   105
wenzelm@12778
   106
wenzelm@12778
   107
(* token translations *)
wenzelm@12778
   108
wenzelm@12778
   109
local
wenzelm@12778
   110
wenzelm@17217
   111
fun end_tag () = special "350";
wenzelm@17217
   112
val class_tag = ("class", fn () => special "351");
wenzelm@17217
   113
val tfree_tag = ("tfree", fn () => special "352");
wenzelm@17217
   114
val tvar_tag = ("tvar", fn () => special "353");
wenzelm@17217
   115
val free_tag = ("free", fn () => special "354");
wenzelm@17217
   116
val bound_tag = ("bound", fn () => special "355");
wenzelm@17217
   117
val var_tag = ("var", fn () => special "356");
wenzelm@17217
   118
val skolem_tag = ("skolem", fn () => special "357");
wenzelm@12778
   119
wenzelm@12778
   120
fun xml_atom kind x = XML.element "atom" [("kind", kind)] [XML.text x];
wenzelm@12778
   121
wenzelm@12778
   122
fun tagit (kind, bg_tag) x =
wenzelm@16534
   123
 (if Output.has_mode pgmlatomsN then xml_atom kind x
wenzelm@17217
   124
  else bg_tag () ^ x ^ end_tag (), real (Symbol.length (Symbol.explode x)));
wenzelm@12778
   125
wenzelm@12778
   126
fun free_or_skolem x =
wenzelm@20081
   127
  (case try Name.dest_skolem x of
skalberg@15531
   128
    NONE => tagit free_tag x
skalberg@15531
   129
  | SOME x' => tagit skolem_tag x');
wenzelm@12778
   130
wenzelm@12778
   131
fun var_or_skolem s =
wenzelm@15985
   132
  (case Syntax.read_variable s of
wenzelm@15985
   133
    SOME (x, i) =>
wenzelm@20081
   134
      (case try Name.dest_skolem x of
skalberg@15531
   135
        NONE => tagit var_tag s
wenzelm@15992
   136
      | SOME x' => tagit skolem_tag
wenzelm@15992
   137
          (setmp show_question_marks true Syntax.string_of_vname (x', i)))
wenzelm@15985
   138
  | NONE => tagit var_tag s);
wenzelm@12778
   139
wenzelm@12778
   140
val proof_general_trans =
wenzelm@12778
   141
 Syntax.tokentrans_mode proof_generalN
wenzelm@12778
   142
  [("class", tagit class_tag),
wenzelm@12778
   143
   ("tfree", tagit tfree_tag),
wenzelm@12778
   144
   ("tvar", tagit tvar_tag),
wenzelm@12778
   145
   ("free", free_or_skolem),
wenzelm@12778
   146
   ("bound", tagit bound_tag),
wenzelm@12778
   147
   ("var", var_or_skolem)];
wenzelm@12778
   148
wenzelm@15801
   149
in
wenzelm@15801
   150
wenzelm@18708
   151
val _ = Context.add_setup (Theory.add_tokentrfuns proof_general_trans);
wenzelm@15801
   152
wenzelm@15801
   153
end;
wenzelm@12778
   154
wenzelm@12778
   155
aspinall@15134
   156
(* assembling PGIP packets *)
aspinall@15134
   157
wenzelm@17217
   158
val pgip_refid  = ref NONE: string option ref;
wenzelm@16534
   159
val pgip_refseq = ref NONE: string option ref;
wenzelm@12778
   160
wenzelm@12778
   161
local
aspinall@16821
   162
  val pgip_class  = "pg"
aspinall@16821
   163
  val pgip_tag = "Isabelle/Isar"
aspinall@16821
   164
  val pgip_id = ref ""
aspinall@16821
   165
  val pgip_seq = ref 0
aspinall@16821
   166
  fun pgip_serial () = inc pgip_seq
wenzelm@12778
   167
wenzelm@16534
   168
  fun assemble_pgips pgips =
wenzelm@16534
   169
    XML.element
wenzelm@16534
   170
      "pgip"
aspinall@16821
   171
      ([("tag",    pgip_tag),
aspinall@17407
   172
        ("class",  pgip_class),
wenzelm@17217
   173
        ("seq",    string_of_int (pgip_serial())),
aspinall@16821
   174
        ("id",     !pgip_id)] @
wenzelm@19473
   175
       the_default [] (Option.map (single o (pair "destid")) (! pgip_refid)) @
aspinall@16821
   176
       (* destid=refid since Isabelle only communicates back to sender,
aspinall@16821
   177
          so we may omit refid from attributes.
wenzelm@19473
   178
       the_default [] (Option.map (single o (pair "refid"))  (! pgip_refid)) @
aspinall@16821
   179
       *)
wenzelm@19473
   180
       the_default [] (Option.map (single o (pair "refseq")) (! pgip_refseq)))
wenzelm@16534
   181
      pgips;
aspinall@16821
   182
wenzelm@13526
   183
in
wenzelm@12778
   184
wenzelm@17217
   185
fun init_pgip_session_id () =
aspinall@16821
   186
    pgip_id := getenv "HOSTNAME" ^ "/" ^ getenv "USER" ^ "/" ^
aspinall@16821
   187
               getenv "ISABELLE_PID" ^ "/" ^ Time.toString (Time.now ())
wenzelm@17217
   188
aspinall@16821
   189
aspinall@16821
   190
fun matching_pgip_id id = (id = !pgip_id)
aspinall@16821
   191
wenzelm@16534
   192
fun decorated_output bg en prfx =
wenzelm@16534
   193
  writeln_default o enclose bg en o prefix_lines prfx;
aspinall@15134
   194
wenzelm@16534
   195
(* FIXME: see Rev 1.48 [PG CVS] for cleaner version of this which can be used
wenzelm@16534
   196
   for PG 4.0 which processes PGIP without needing special chars *)
wenzelm@16534
   197
fun issue_pgips ps =
wenzelm@16534
   198
  if pgip_emacs_compatibility() then
wenzelm@16534
   199
    decorated_output (*add urgent message annotation*)
wenzelm@17217
   200
      (special "360") (special "361") ""
wenzelm@16534
   201
      (assemble_pgips ps)
wenzelm@16534
   202
  else
wenzelm@16534
   203
    writeln_default (assemble_pgips ps);
aspinall@15134
   204
wenzelm@16534
   205
fun assemble_pgip resp attrs s = assemble_pgips [XML.element resp attrs [s]];
wenzelm@16534
   206
fun assemble_pgipe resp attrs = assemble_pgips [XML.element resp attrs []];
aspinall@15134
   207
wenzelm@16534
   208
(* FIXME: need to add stuff to gather PGIPs here *)
wenzelm@16534
   209
fun issue_pgip resp attrs txt =
wenzelm@16534
   210
  if pgip_emacs_compatibility () then
wenzelm@16534
   211
    decorated_output (*add urgent message annotation*)
wenzelm@17217
   212
      (special "360") (special "361") ""
wenzelm@16534
   213
      (assemble_pgip resp attrs txt)
wenzelm@16534
   214
  else
wenzelm@16534
   215
    writeln_default (assemble_pgip resp attrs txt);
aspinall@15134
   216
wenzelm@16534
   217
(* FIXME: temporarily to support PG 3.4 *)
wenzelm@16534
   218
fun issue_pgip_maybe_decorated bg en resp attrs s =
wenzelm@16534
   219
  if pgip_emacs_compatibility () then
wenzelm@16534
   220
    (*in PGIP mode, but using escape characters as well*)
wenzelm@16534
   221
    writeln_default (enclose bg en (assemble_pgip resp attrs s))
wenzelm@16534
   222
  else
wenzelm@16534
   223
    issue_pgip resp attrs s;
aspinall@15134
   224
wenzelm@16534
   225
fun issue_pgipe resp attrs = writeln_default (assemble_pgipe resp attrs);
wenzelm@16534
   226
wenzelm@16534
   227
end;
wenzelm@16534
   228
aspinall@15134
   229
aspinall@15134
   230
(* messages and notification *)
aspinall@15134
   231
aspinall@15173
   232
local
wenzelm@16534
   233
  val delay_msgs = ref false;   (*true: accumulate messages*)
wenzelm@16534
   234
  val delayed_msgs = ref [];
aspinall@15173
   235
in
aspinall@15134
   236
wenzelm@16534
   237
fun message resp attrs bg en prfx s =
wenzelm@16534
   238
  if pgip () then
wenzelm@16534
   239
   (if (! delay_msgs) then
wenzelm@16534
   240
      delayed_msgs := (resp, attrs, prefix_lines prfx s) :: ! delayed_msgs (*NB: no decs*)
wenzelm@16534
   241
    else
wenzelm@16534
   242
      issue_pgip_maybe_decorated bg en resp attrs
wenzelm@16534
   243
        (XML.element "pgmltext" [] [prefix_lines prfx s]))
wenzelm@16534
   244
  else decorated_output bg en prfx s;
aspinall@15173
   245
wenzelm@16534
   246
fun start_delay_msgs () = (set delay_msgs; delayed_msgs := []);
aspinall@15173
   247
wenzelm@16534
   248
fun end_delayed_msgs () = (reset delay_msgs;
wenzelm@16534
   249
  (! delayed_msgs) |> map (fn (resp, attrs, s) =>
wenzelm@16534
   250
    XML.element resp attrs [XML.element "pgmltext" [] [s]]));
wenzelm@16534
   251
wenzelm@16534
   252
end;
aspinall@15134
   253
aspinall@15134
   254
local
wenzelm@16534
   255
  val display_area = ("area", "display");
wenzelm@16534
   256
  val message_area = ("area", "message");
wenzelm@16534
   257
  val internal_category = ("messagecategory", "internal");
wenzelm@16534
   258
  val info_category = ("messagecategory", "information");
wenzelm@16534
   259
  val tracing_category = ("messagecategory", "tracing");
wenzelm@16534
   260
  val urgent_indication = ("urgent", "y");
wenzelm@16534
   261
  val nonfatal = ("fatality", "nonfatal");
wenzelm@16534
   262
  val fatal = ("fatality", "fatal");
wenzelm@16534
   263
  val panic = ("fatality", "panic");
aspinall@15134
   264
wenzelm@16534
   265
  val thyname_attr = pair "thyname";
wenzelm@16534
   266
  val url_attr = pair "url";
aspinall@21514
   267
  fun localfile_url_attr abspath = url_attr ("file:" ^ abspath);
wenzelm@16534
   268
in
wenzelm@12778
   269
wenzelm@12778
   270
fun setup_messages () =
wenzelm@17217
   271
 (writeln_fn := (fn s => message "normalresponse" [message_area] "" "" "" s);
wenzelm@17217
   272
  priority_fn := (fn s => message "normalresponse" [message_area, urgent_indication]
wenzelm@17217
   273
    (special "360") (special "361") "" s);
wenzelm@17217
   274
  tracing_fn := (fn s => message "normalresponse"  [message_area, tracing_category]
wenzelm@17217
   275
    (special "360" ^ special "375") (special "361") "" s);
wenzelm@17217
   276
  info_fn := (fn s => message "normalresponse" [message_area, info_category]
wenzelm@17217
   277
    (special "362") (special "363") "+++ " s);
wenzelm@17217
   278
  debug_fn := (fn s => message "normalresponse" [message_area, internal_category]
wenzelm@17217
   279
    (special "362") (special "363") "+++ " s);
wenzelm@17217
   280
  warning_fn := (fn s => message "errorresponse" [nonfatal]
wenzelm@17217
   281
    (special "362") (special "363") "### " s);
wenzelm@17217
   282
  error_fn := (fn s => message "errorresponse" [fatal]
wenzelm@17217
   283
    (special "364") (special "365") "*** " s);
wenzelm@17217
   284
  panic_fn := (fn s => message "errorresponse" [panic]
wenzelm@17217
   285
    (special "364") (special "365") "!!! " s));
aspinall@15134
   286
aspinall@15134
   287
aspinall@15400
   288
(* accumulate printed output in a single PGIP response (inside <pgmltext>) *)
aspinall@15134
   289
wenzelm@16534
   290
fun with_displaywrap (elt, attrs) dispfn =
wenzelm@16534
   291
  let
wenzelm@16534
   292
    val lines = ref ([]: string list);
wenzelm@16534
   293
    fun wlgrablines s = lines := s :: ! lines;
wenzelm@16534
   294
  in
wenzelm@16534
   295
    setmp writeln_fn wlgrablines dispfn ();
aspinall@16798
   296
    (* IMPORTANT FIXME: XML.element here too inefficient, should use stream output *)
wenzelm@16534
   297
    issue_pgip elt attrs (XML.element "pgmltext" [] (! lines))
wenzelm@16534
   298
  end;
wenzelm@12778
   299
wenzelm@17217
   300
fun emacs_notify s = decorated_output (special "360") (special "361") "" s;
aspinall@15134
   301
wenzelm@16534
   302
fun tell_clear_goals () =
wenzelm@16534
   303
  if pgip () then
wenzelm@16534
   304
    issue_pgipe "cleardisplay" [display_area]
wenzelm@16534
   305
  else
wenzelm@16534
   306
    emacs_notify "Proof General, please clear the goals buffer.";
wenzelm@16534
   307
wenzelm@16534
   308
fun tell_clear_response () =
wenzelm@16534
   309
  if pgip () then
wenzelm@16534
   310
    issue_pgipe "cleardisplay" [message_area]
wenzelm@16534
   311
  else
wenzelm@16534
   312
    emacs_notify "Proof General, please clear the response buffer.";
wenzelm@12778
   313
wenzelm@16534
   314
fun tell_file_loaded path =
wenzelm@16534
   315
  if pgip () then
aspinall@16788
   316
    issue_pgipe "informfileloaded"
aspinall@21514
   317
      [localfile_url_attr  (XML.text (File.platform_path 
aspinall@21514
   318
					  (File.full_path path)))]
wenzelm@16534
   319
  else
aspinall@21514
   320
    emacs_notify ("Proof General, this file is loaded: " ^ 
aspinall@21514
   321
		  quote (File.platform_path path));
aspinall@15134
   322
wenzelm@16534
   323
fun tell_file_retracted path =
wenzelm@16534
   324
  if pgip() then
aspinall@16788
   325
    issue_pgipe "informfileretracted"
aspinall@21514
   326
      [localfile_url_attr  (XML.text (File.platform_path 
aspinall@21514
   327
					  (File.full_path path)))]
wenzelm@16534
   328
  else
aspinall@21514
   329
    emacs_notify ("Proof General, you can unlock the file " 
aspinall@21514
   330
		  ^ quote (File.platform_path path));
wenzelm@12778
   331
wenzelm@12778
   332
wenzelm@12778
   333
(* theory / proof state output *)
wenzelm@12778
   334
wenzelm@12778
   335
local
wenzelm@12778
   336
wenzelm@16534
   337
fun tmp_markers f =
wenzelm@17217
   338
  setmp Display.current_goals_markers (special "366", special "367", "") f ();
wenzelm@12778
   339
wenzelm@16534
   340
fun statedisplay prts =
wenzelm@16534
   341
  issue_pgip "proofstate" []
wenzelm@16534
   342
    (XML.element "pgml" []
wenzelm@16534
   343
      [XML.element "statedisplay" [] [Pretty.output (Pretty.chunks prts)]]);
wenzelm@17217
   344
wenzelm@16534
   345
fun print_current_goals n m st =
wenzelm@16534
   346
  if pgml () then statedisplay (Display.pretty_current_goals n m st)
wenzelm@16534
   347
  else tmp_markers (fn () => Display.print_current_goals_default n m st);
wenzelm@13545
   348
wenzelm@16534
   349
fun print_state b st =
wenzelm@16534
   350
  if pgml () then statedisplay (Toplevel.pretty_state b st)
wenzelm@16534
   351
  else tmp_markers (fn () => Toplevel.print_state_default b st);
wenzelm@16534
   352
wenzelm@13526
   353
in
wenzelm@13526
   354
wenzelm@16534
   355
fun setup_state () =
wenzelm@16534
   356
  (Display.print_current_goals_fn := print_current_goals;
wenzelm@16534
   357
   Toplevel.print_state_fn := print_state;
wenzelm@16534
   358
   (* FIXME: check next octal char won't appear in pgip? *)
wenzelm@17217
   359
   Toplevel.prompt_state_fn := (fn s => suffix (special "372")
wenzelm@17217
   360
     (Toplevel.prompt_state_default s)));
berghofe@13728
   361
wenzelm@16534
   362
end;
wenzelm@16534
   363
wenzelm@16534
   364
end;
berghofe@13728
   365
wenzelm@16022
   366
wenzelm@12778
   367
(* misc commands for ProofGeneral/isa *)
wenzelm@12778
   368
wenzelm@12778
   369
fun thms_containing ss =
wenzelm@16534
   370
  FindTheorems.print_theorems (ProofContext.init (the_context ())) NONE NONE
wenzelm@16022
   371
    (map (fn s => (true, FindTheorems.Pattern s)) ss);
wenzelm@12778
   372
wenzelm@12778
   373
val welcome = priority o Session.welcome;
wenzelm@12778
   374
val help = welcome;
wenzelm@12778
   375
val show_context = Context.the_context;
wenzelm@12778
   376
wenzelm@17959
   377
fun kill_goal () = (OldGoals.reset_goals (); tell_clear_goals ());
wenzelm@12778
   378
wenzelm@12778
   379
fun no_print_goals f = setmp Display.print_current_goals_fn (fn _ => fn _ => fn _ => ()) f;
wenzelm@12778
   380
wenzelm@12778
   381
fun repeat_undo 0 = ()
wenzelm@12778
   382
  | repeat_undo 1 = undo ()
wenzelm@12778
   383
  | repeat_undo n = (no_print_goals undo (); repeat_undo (n - 1));
wenzelm@12778
   384
wenzelm@12778
   385
aspinall@15134
   386
(* theory loader actions *)
aspinall@15134
   387
aspinall@15134
   388
local
aspinall@15134
   389
aspinall@15134
   390
fun trace_action action name =
aspinall@15134
   391
  if action = ThyInfo.Update then
skalberg@15570
   392
    List.app tell_file_loaded (ThyInfo.loaded_files name)
aspinall@15134
   393
  else if action = ThyInfo.Outdate orelse action = ThyInfo.Remove then
aspinall@21538
   394
    List.app tell_file_retracted (ThyInfo.loaded_files name)
aspinall@15134
   395
  else ();
aspinall@15134
   396
aspinall@15134
   397
in
aspinall@15134
   398
  fun setup_thy_loader () = ThyInfo.add_hook trace_action;
skalberg@15570
   399
  fun sync_thy_loader () = List.app (trace_action ThyInfo.Update) (ThyInfo.names ());
aspinall@15134
   400
end;
aspinall@15134
   401
aspinall@15134
   402
aspinall@15134
   403
(* prepare theory context *)
aspinall@15134
   404
aspinall@15134
   405
val thy_name = Path.pack o #1 o Path.split_ext o Path.base o Path.unpack;
wenzelm@16534
   406
wenzelm@16534
   407
(* FIXME general treatment of tracing*)
wenzelm@16534
   408
val update_thy_only = setmp MetaSimplifier.trace_simp false ThyInfo.update_thy_only;
aspinall@15134
   409
wenzelm@16440
   410
fun dynamic_context () =
aspinall@15134
   411
  (case Context.get_context () of
wenzelm@16440
   412
    SOME thy => "  Using current (dynamic!) one: " ^ quote (Context.theory_name thy)
skalberg@15531
   413
  | NONE => "");
aspinall@15134
   414
aspinall@15134
   415
fun try_update_thy_only file =
aspinall@15134
   416
  ThyLoad.cond_add_path (Path.dir (Path.unpack file)) (fn () =>
aspinall@15134
   417
    let val name = thy_name file in
wenzelm@16534
   418
      if is_some (ThyLoad.check_file NONE (ThyLoad.thy_path name))
aspinall@15134
   419
      then update_thy_only name
wenzelm@16440
   420
      else warning ("Unkown theory context of ML file." ^ dynamic_context ())
aspinall@15134
   421
    end) ();
aspinall@15134
   422
aspinall@15134
   423
aspinall@15134
   424
(* get informed about files *)
aspinall@15134
   425
wenzelm@16534
   426
val inform_file_retracted = ThyInfo.if_known_thy ThyInfo.remove_thy o thy_name;
wenzelm@16534
   427
val inform_file_processed = ThyInfo.if_known_thy ThyInfo.touch_child_thys o thy_name;
wenzelm@16534
   428
val openfile_retract = Output.no_warnings (ThyInfo.if_known_thy ThyInfo.remove_thy) o thy_name;
aspinall@15629
   429
aspinall@15134
   430
fun proper_inform_file_processed file state =
aspinall@15134
   431
  let val name = thy_name file in
aspinall@15134
   432
    if Toplevel.is_toplevel state andalso ThyInfo.known_thy name then
aspinall@15134
   433
     (ThyInfo.touch_child_thys name;
wenzelm@18678
   434
      ThyInfo.pretend_use_thy_only name handle ERROR msg =>
aspinall@15134
   435
       (warning msg; warning ("Failed to register theory: " ^ quote name);
aspinall@15134
   436
        tell_file_retracted (Path.base (Path.unpack file))))
aspinall@15134
   437
    else raise Toplevel.UNDEF
aspinall@15134
   438
  end;
aspinall@15134
   439
aspinall@15134
   440
fun vacuous_inform_file_processed file state =
aspinall@15134
   441
 (warning ("No theory " ^ quote (thy_name file));
aspinall@15134
   442
  tell_file_retracted (Path.base (Path.unpack file)));
aspinall@15134
   443
aspinall@15134
   444
wenzelm@12778
   445
(* restart top-level loop (keeps most state information) *)
wenzelm@12778
   446
wenzelm@12778
   447
local
wenzelm@12778
   448
wenzelm@12778
   449
fun restart isar =
wenzelm@12778
   450
 (if isar then tell_clear_goals () else kill_goal ();
wenzelm@12778
   451
  tell_clear_response ();
wenzelm@12778
   452
  welcome ());
wenzelm@12778
   453
wenzelm@12778
   454
in
wenzelm@12778
   455
wenzelm@12778
   456
fun isa_restart () = restart false;
wenzelm@12778
   457
fun isar_restart () = (sync_thy_loader (); restart true; raise Toplevel.RESTART);
wenzelm@12778
   458
wenzelm@12778
   459
end;
wenzelm@12778
   460
wenzelm@12833
   461
fun full_proofs true = proofs := 2
wenzelm@12833
   462
  | full_proofs false = proofs := 1;
wenzelm@12833
   463
wenzelm@12833
   464
aspinall@15134
   465
(* theorem dependency output *)
aspinall@15134
   466
aspinall@15134
   467
local
aspinall@15134
   468
aspinall@15134
   469
val spaces_quote = space_implode " " o map quote;
aspinall@15134
   470
aspinall@16789
   471
(* FIXME: investigate why dependencies at the moment include themselves! *)
wenzelm@16534
   472
fun thm_deps_message (thms, deps) =
wenzelm@16534
   473
  if pgip() then
wenzelm@16534
   474
    issue_pgips
wenzelm@16534
   475
      [XML.element
wenzelm@16534
   476
        "metainforesponse"  (* FIXME: get thy name from info here? *)
wenzelm@16534
   477
        [("infotype", "isabelle_theorem_dependencies")]
wenzelm@16534
   478
        [XML.element "value" [("name", "thms")] [XML.text thms],
wenzelm@16534
   479
         XML.element "value" [("name", "deps")] [XML.text deps]]]
wenzelm@16534
   480
  else emacs_notify ("Proof General, theorem dependencies of " ^ thms ^ " are " ^ deps);
aspinall@15134
   481
wenzelm@16534
   482
fun tell_thm_deps ths = conditional (Output.has_mode thm_depsN) (fn () =>
wenzelm@16534
   483
  let
wenzelm@16534
   484
    val names = filter_out (equal "") (map Thm.name_of_thm ths);
wenzelm@16534
   485
    val deps = filter_out (equal "")
berghofe@17018
   486
      (Symtab.keys (fold Proofterm.thms_of_proof
berghofe@17018
   487
        (map Thm.proof_of ths) Symtab.empty));
wenzelm@16534
   488
  in
wenzelm@16534
   489
    if null names orelse null deps then ()
wenzelm@16534
   490
    else thm_deps_message (spaces_quote names, spaces_quote deps)
wenzelm@16534
   491
  end);
aspinall@15134
   492
aspinall@15134
   493
in
aspinall@15134
   494
aspinall@15134
   495
fun setup_present_hook () =
wenzelm@19482
   496
  Present.add_hook (fn _ => fn res => tell_thm_deps (maps #2 res));
aspinall@15134
   497
aspinall@15134
   498
end;
aspinall@15134
   499
aspinall@15134
   500
wenzelm@16534
   501
wenzelm@16534
   502
(** preferences **)
aspinall@15134
   503
aspinall@15134
   504
local
aspinall@15134
   505
wenzelm@20364
   506
fun signed_string_of_int i =
wenzelm@20364
   507
  if i < 0 then "-" ^ string_of_int (~ i) else string_of_int i;
wenzelm@20364
   508
wenzelm@20299
   509
val pgipint = XML.element "pgipint" [] [];
wenzelm@16534
   510
val pgipnat = XML.element "pgipint" [("min", "0")] [];
wenzelm@16534
   511
fun pgipnatmax max = XML.element "pgipint" [("min", "0"), ("max", string_of_int max)] [];
wenzelm@16534
   512
val pgipbool = XML.element "pgipbool" [] [];
wenzelm@16534
   513
wenzelm@16534
   514
fun with_default f = (f (), f);
wenzelm@16534
   515
aspinall@15134
   516
in
aspinall@15134
   517
wenzelm@20299
   518
fun int_option r = (pgipint,
wenzelm@20364
   519
  with_default (fn () => signed_string_of_int (! r)),
wenzelm@20299
   520
  (fn s => (case Syntax.read_int s of
wenzelm@20299
   521
      NONE => error ("int_option: illegal value: " ^ s)
wenzelm@20299
   522
    | SOME i => r := i)));
wenzelm@20299
   523
aspinall@15134
   524
fun nat_option r = (pgipnat,
wenzelm@16534
   525
  with_default (fn () => string_of_int (! r)),
aspinall@15134
   526
  (fn s => (case Syntax.read_nat s of
wenzelm@16534
   527
      NONE => error ("nat_option: illegal value: " ^ s)
wenzelm@16534
   528
    | SOME i => r := i)));
aspinall@15134
   529
aspinall@15134
   530
fun bool_option r = (pgipbool,
wenzelm@16534
   531
  with_default (fn () => Bool.toString (! r)),
aspinall@15134
   532
  (fn "false" => r := false | "true" => r := true
wenzelm@16534
   533
    | x => error ("bool_option: illegal value: " ^ x)));
aspinall@15134
   534
aspinall@15134
   535
val proof_option = (pgipbool,
wenzelm@16534
   536
  with_default (fn () => Bool.toString (! proofs >= 2)),
aspinall@15134
   537
  (fn "false" => proofs := 1 | "true" => proofs := 2
wenzelm@16534
   538
    | x => error ("proof_option: illegal value: " ^ x)));
aspinall@15134
   539
aspinall@15134
   540
val thm_deps_option = (pgipbool,
wenzelm@16534
   541
  with_default (fn () => Bool.toString (Output.has_mode thm_depsN)),
wenzelm@17217
   542
  (fn "false" => change print_mode (remove (op =) thm_depsN)
wenzelm@17217
   543
    | "true" => change print_mode (insert (op =) thm_depsN)
wenzelm@16534
   544
    | x => error ("thm_deps_option: illegal value: " ^ x)));
aspinall@15134
   545
wenzelm@16534
   546
local
wenzelm@16534
   547
  val pg_print_depth_val = ref 10;
wenzelm@16534
   548
  fun pg_print_depth n = (print_depth n; pg_print_depth_val := n)
aspinall@15134
   549
in
wenzelm@16534
   550
aspinall@15134
   551
val print_depth_option = (pgipnat,
wenzelm@16534
   552
  with_default (fn () => string_of_int (! pg_print_depth_val)),
aspinall@15134
   553
  (fn s => (case Syntax.read_nat s of
wenzelm@16534
   554
      NONE => error ("print_depth_option: illegal value: " ^ s)
wenzelm@16534
   555
    | SOME i => pg_print_depth i)));
wenzelm@16534
   556
end;
aspinall@15134
   557
wenzelm@16534
   558
val preferences = ref
aspinall@15134
   559
  [("Display",
wenzelm@16534
   560
    [("show-types",
wenzelm@16534
   561
      ("Include types in display of Isabelle terms",
aspinall@15134
   562
       bool_option show_types)),
wenzelm@16534
   563
     ("show-sorts",
wenzelm@16534
   564
      ("Include sorts in display of Isabelle terms",
aspinall@15134
   565
       bool_option show_sorts)),
wenzelm@16534
   566
     ("show-consts",
aspinall@15134
   567
      ("Show types of consts in Isabelle goal display",
aspinall@15134
   568
       bool_option show_consts)),
wenzelm@16534
   569
     ("long-names",
wenzelm@16534
   570
      ("Show fully qualified names in Isabelle terms",
wenzelm@16534
   571
       bool_option long_names)),
wenzelm@16534
   572
     ("show-brackets",
aspinall@15134
   573
      ("Show full bracketing in Isabelle terms",
aspinall@15134
   574
       bool_option show_brackets)),
wenzelm@16534
   575
     ("show-main-goal",
wenzelm@16534
   576
      ("Show main goal in proof state display",
wenzelm@16534
   577
       bool_option Proof.show_main_goal)),
wenzelm@16534
   578
     ("eta-contract",
aspinall@15134
   579
      ("Print terms eta-contracted",
aspinall@15134
   580
       bool_option Syntax.eta_contract))]),
aspinall@15134
   581
   ("Advanced Display",
wenzelm@16534
   582
    [("goals-limit",
aspinall@15134
   583
      ("Setting for maximum number of goals printed",
aspinall@15134
   584
       nat_option goals_limit)),
wenzelm@16534
   585
     ("prems-limit",
aspinall@15134
   586
      ("Setting for maximum number of premises printed",
wenzelm@20299
   587
       int_option ProofContext.prems_limit)),
wenzelm@16534
   588
     ("print-depth",
aspinall@15134
   589
      ("Setting for the ML print depth",
berghofe@15472
   590
       print_depth_option)),
wenzelm@15985
   591
     ("show-question-marks",
berghofe@15472
   592
      ("Show leading question mark of variable name",
wenzelm@15985
   593
       bool_option show_question_marks))]),
aspinall@15134
   594
   ("Tracing",
wenzelm@16534
   595
    [("trace-simplifier",
aspinall@15134
   596
      ("Trace simplification rules.",
aspinall@15134
   597
       bool_option trace_simp)),
wenzelm@17417
   598
     ("trace-simplifier-depth",
wenzelm@17417
   599
      ("Trace simplifier depth limit.",
wenzelm@17417
   600
       nat_option trace_simp_depth_limit)),
wenzelm@16534
   601
     ("trace-rules",
wenzelm@16534
   602
      ("Trace application of the standard rules",
wenzelm@16534
   603
       bool_option trace_rules)),
wenzelm@16534
   604
     ("trace-unification",
aspinall@15134
   605
      ("Output error diagnostics during unification",
aspinall@15134
   606
       bool_option Pattern.trace_unify_fail)),
wenzelm@16534
   607
     ("global-timing",
aspinall@15134
   608
      ("Whether to enable timing in Isabelle.",
aspinall@15134
   609
       bool_option Output.timing))]),
wenzelm@16534
   610
   ("Proof",
wenzelm@16534
   611
    [("quick-and-dirty",
wenzelm@16534
   612
      ("Take a few short cuts",
aspinall@15134
   613
       bool_option quick_and_dirty)),
wenzelm@16534
   614
     ("full-proofs",
aspinall@15134
   615
      ("Record full proof objects internally",
aspinall@15134
   616
       proof_option)),
wenzelm@16534
   617
     ("theorem-dependencies",
aspinall@15134
   618
       ("Track theorem dependencies within Proof General",
wenzelm@16534
   619
        thm_deps_option)),
wenzelm@16534
   620
     ("skip-proofs",
wenzelm@16816
   621
      ("Ignore proof scripts (interactive-only)",
berghofe@15238
   622
       bool_option Toplevel.skip_proofs))])
aspinall@15134
   623
   ];
wenzelm@16534
   624
end;
wenzelm@16534
   625
aspinall@21464
   626
(** lexicalstructure element with keywords (PGIP version of elisp keywords file) **)
aspinall@21464
   627
aspinall@21464
   628
fun lexicalstructure_keywords () = 
aspinall@21464
   629
    let val commands = OuterSyntax.dest_keywords ()
aspinall@21464
   630
	fun category_of k = if (k mem commands) then "major" else "minor"
aspinall@21464
   631
         (* NB: we might filter to only include words like elisp case (OuterSyntax.is_keyword). *)
aspinall@21464
   632
    	fun keyword_elt (keyword,help,kind,_) = 
aspinall@21464
   633
  	    XML.element "keyword" [("word", keyword), ("category", category_of kind)]
aspinall@21464
   634
	  	    [XML.element "shorthelp" [] [XML.text help]]
aspinall@21464
   635
        in 	    	    
aspinall@21464
   636
            (* Also, note we don't call init_outer_syntax here to add interface commands,
aspinall@21464
   637
            but they should never appear in scripts anyway so it shouldn't matter *)
aspinall@21464
   638
            XML.element "lexicalstructure" [] (map keyword_elt (OuterSyntax.dest_parsers()))
aspinall@21464
   639
        end
aspinall@21464
   640
aspinall@21464
   641
(* TODO: we can issue a lexicalstructure/keyword when the syntax gets extended dynamically;
aspinall@21464
   642
   hooks needed in outer_syntax.ML to do that. *)
aspinall@21464
   643
aspinall@15134
   644
aspinall@15134
   645
(* Configuration: GUI config, proverinfo messages *)
aspinall@15134
   646
aspinall@17732
   647
aspinall@17732
   648
fun orenv v d = case (getenv v) of "" => d  | s => s
aspinall@17732
   649
aspinall@15134
   650
local
aspinall@17732
   651
    fun config_file()  = orenv "ISABELLE_PGIPCONFIG" "~~/lib/ProofGeneral/pgip_isar.xml"
aspinall@17732
   652
    fun isabelle_www() = orenv "ISABELLE_HOMEPAGE" "http://isabelle.in.tum.de/"
aspinall@15134
   653
in
aspinall@15134
   654
fun send_pgip_config () =
wenzelm@16534
   655
    let
aspinall@17732
   656
        val path = Path.unpack (config_file())
wenzelm@16534
   657
        val exists = File.exists path
wenzelm@16534
   658
        val proverinfo =
wenzelm@16534
   659
            XML.element "proverinfo"
aspinall@17732
   660
              [("name",     	 "Isabelle"), 
aspinall@17732
   661
	       ("version",  	 version),
aspinall@17732
   662
	       ("instance", 	 Session.name()), 
aspinall@17739
   663
	       ("descr",	 "The Isabelle/Isar theorem prover"),
aspinall@17732
   664
	       ("url",      	 isabelle_www()),   
aspinall@17732
   665
	       ("filenameextns", ".thy;")]
aspinall@17739
   666
            []
aspinall@15134
   667
    in
wenzelm@16534
   668
        if exists then
aspinall@21464
   669
            (issue_pgips [proverinfo]; 
aspinall@21464
   670
	     issue_pgips [File.read path];
aspinall@21464
   671
	     issue_pgips [lexicalstructure_keywords()])
wenzelm@18678
   672
        else Output.panic ("PGIP configuration file \"" ^ config_file() ^ "\" not found")
aspinall@15134
   673
    end;
aspinall@15134
   674
end
aspinall@15134
   675
aspinall@15134
   676
aspinall@15629
   677
(* Reveal some information about prover state *)
aspinall@15629
   678
fun send_informguise (openfile, opentheory, openproofpos) =
wenzelm@16534
   679
    let val guisefile =
wenzelm@16534
   680
            case openfile of SOME f => [XML.element "guisefile"
wenzelm@16534
   681
                                                    [("url",Url.pack (Url.File (Path.unpack f)))] []]
wenzelm@16534
   682
                           | _ => []
wenzelm@16534
   683
        val guisetheory =
wenzelm@16534
   684
            case opentheory of SOME t => [XML.element "guisetheory" [("thyname", t)] []]
wenzelm@16534
   685
                             | _ => []
wenzelm@16534
   686
        val guiseproof =
wenzelm@16534
   687
            case openproofpos of SOME i => [XML.element "guiseproof" [("proofpos", string_of_int i)] []]
wenzelm@16534
   688
                               | _ => []
wenzelm@16534
   689
    in
wenzelm@16534
   690
        issue_pgips [XML.element "informguise" [] (guisefile @ guisetheory @ guiseproof)]
wenzelm@16534
   691
    end
aspinall@15629
   692
aspinall@15629
   693
aspinall@15134
   694
(* PGIP identifier tables (prover objects). [incomplete] *)
aspinall@15134
   695
aspinall@15134
   696
local
aspinall@15134
   697
    val objtype_thy  = "theory"
aspinall@15134
   698
    val objtype_thm  = "theorem"
aspinall@15134
   699
    val objtype_term = "term"
aspinall@15134
   700
    val objtype_type = "type"
wenzelm@16534
   701
wenzelm@16534
   702
    fun xml_idtable ty ctx ids =
wenzelm@16534
   703
        let
skalberg@15531
   704
            fun ctx_attr (SOME c)= [("context", c)]
skalberg@15531
   705
              | ctx_attr NONE    = []
wenzelm@16534
   706
            fun xmlid x = XML.element "identifier" [] [XML.text x];
wenzelm@16534
   707
        in
wenzelm@16534
   708
            XML.element "idtable" (("objtype", ty)::ctx_attr ctx)
wenzelm@16534
   709
                                  (map xmlid ids)
wenzelm@16534
   710
        end
aspinall@15134
   711
in
aspinall@15134
   712
aspinall@15134
   713
fun setids t = issue_pgip "setids" [] t
aspinall@15134
   714
fun addids t = issue_pgip "addids" [] t
aspinall@15134
   715
fun delids t = issue_pgip "delids" [] t
aspinall@15134
   716
skalberg@15531
   717
fun delallids ty = setids (xml_idtable ty NONE [])
aspinall@15134
   718
aspinall@15134
   719
fun send_thy_idtable ctx thys = setids (xml_idtable objtype_thy ctx thys)
aspinall@15134
   720
fun clear_thy_idtable () = delallids objtype_thy
aspinall@15134
   721
wenzelm@16534
   722
fun send_thm_idtable ctx thy =
aspinall@15134
   723
    addids (xml_idtable objtype_thm ctx (map fst (PureThy.thms_of thy)));
aspinall@15134
   724
aspinall@15134
   725
fun clear_thm_idtable () = delallids objtype_thm
aspinall@15134
   726
aspinall@15134
   727
(* fun send_type_idtable thy = TODO, it's a bit low-level messy
aspinall@15134
   728
   & maybe not so useful anyway *)
wenzelm@16534
   729
aspinall@15134
   730
end
aspinall@15134
   731
aspinall@15134
   732
(* Response to interface queries about known objects *)
aspinall@15134
   733
aspinall@15134
   734
local
aspinall@15134
   735
 val topthy = Toplevel.theory_of o Toplevel.get_state
wenzelm@16486
   736
 fun pthm thy name = print_thm (get_thm thy (Name name))
aspinall@15134
   737
aspinall@15134
   738
 fun idvalue tp nm = ("idvalue",[("objtype",tp),("name",nm)])
aspinall@15134
   739
in
aspinall@16798
   740
(* FIXME: add askids for "file" here, which returns single theory with same name *)
skalberg@15531
   741
fun askids (NONE, SOME "theory")  = send_thy_idtable NONE (ThyInfo.names())
skalberg@15531
   742
  | askids (NONE, NONE) =  send_thy_idtable NONE (ThyInfo.names())
aspinall@15134
   743
                           (* only theories known in top context *)
skalberg@15531
   744
  | askids (SOME thy, SOME "theory") = send_thy_idtable (SOME thy) (ThyInfo.get_preds thy)
skalberg@15531
   745
  | askids (SOME thy, SOME "theorem") = send_thm_idtable (SOME thy) (ThyInfo.get_theory thy)
skalberg@15531
   746
  | askids (SOME thy, NONE) = (send_thy_idtable (SOME thy) (ThyInfo.get_preds thy);
wenzelm@16534
   747
                               send_thm_idtable (SOME thy) (ThyInfo.get_theory thy))
skalberg@15531
   748
  | askids (_, SOME ot) = error ("No objects of type "^(quote ot)^" are available here.")
aspinall@15134
   749
wenzelm@16534
   750
fun showid (_,        "theory", n) =
aspinall@15134
   751
    with_displaywrap (idvalue "theory" n) (fn ()=>(print_theory (ThyInfo.get_theory n)))
wenzelm@16534
   752
  | showid (SOME thy, "theorem", t) =
aspinall@15134
   753
    with_displaywrap (idvalue "theorem" t) (fn ()=>(pthm (ThyInfo.get_theory thy) t))
wenzelm@16534
   754
  | showid (NONE,     "theorem", t) =
aspinall@15134
   755
    with_displaywrap (idvalue "theorem" t) (fn ()=>pthm (topthy()) t)
aspinall@15134
   756
  | showid (_, ot, _) = error ("Cannot show objects of type "^ot)
aspinall@15134
   757
aspinall@15134
   758
end
aspinall@15629
   759
aspinall@15629
   760
aspinall@21464
   761
aspinall@15134
   762
(** Parsing proof scripts without execution **)
aspinall@15134
   763
aspinall@15146
   764
(* Notes.
aspinall@15146
   765
   This is quite tricky, because 1) we need to put back whitespace which
aspinall@15146
   766
   was removed during parsing so we can provide markup around commands;
aspinall@15146
   767
   2) parsing is intertwined with execution in Isar so we have to repeat
aspinall@15146
   768
   the parsing to extract interesting parts of commands.  The trace of
aspinall@15254
   769
   tokens parsed which is now recorded in each transition (added by
aspinall@15254
   770
   Markus June '04) helps do this, but the mechanism is still a bad mess.
wenzelm@16534
   771
aspinall@15254
   772
   If we had proper parse trees it would be easy, although having a
aspinall@15254
   773
   fixed type of trees might be tricky with Isar's extensible parser.
aspinall@15146
   774
aspinall@15146
   775
   Probably the best solution is to produce the meta-information at
wenzelm@16534
   776
   the same time as the parse, for each command, e.g. by recording a
wenzelm@16534
   777
   list of (name,objtype) pairs which record the bindings created by
wenzelm@16534
   778
   a command.  This would require changing the interfaces in
wenzelm@16534
   779
   outer_syntax.ML (or providing new ones),
aspinall@15146
   780
aspinall@15146
   781
    datatype metainfo = Binding of string * string  (* name, objtype *)
aspinall@15146
   782
aspinall@15146
   783
    val command_withmetainfo: string -> string -> string ->
wenzelm@16534
   784
      (token list ->
wenzelm@16534
   785
       ((Toplevel.transition -> Toplevel.transition) * metainfo list) *
aspinall@15146
   786
       token list) -> parser
aspinall@15254
   787
aspinall@15254
   788
   We'd also like to render terms as they appear in output, but this
wenzelm@16534
   789
   will be difficult because inner syntax is extensible and we don't
aspinall@15254
   790
   have the correct syntax to hand when just doing outer parsing
wenzelm@16534
   791
   without execution.  A reasonable approximation could
aspinall@15254
   792
   perhaps be obtained by using the syntax of the current context.
wenzelm@16534
   793
   However, this would mean more mess trying to pick out terms,
aspinall@15254
   794
   so at this stage a more serious change to the Isar functions
aspinall@15254
   795
   seems necessary.
aspinall@15146
   796
*)
aspinall@15146
   797
aspinall@15134
   798
local
aspinall@15145
   799
    fun markup_text str elt = [XML.element elt [] [XML.text str]]
aspinall@15145
   800
    fun markup_text_attrs str elt attrs = [XML.element elt attrs [XML.text str]]
aspinall@15145
   801
    fun empty elt = [XML.element elt [] []]
aspinall@15145
   802
aspinall@15210
   803
    fun whitespace str = XML.element "whitespace" [] [XML.text str]
aspinall@15208
   804
aspinall@15146
   805
    (* an extra token is needed to terminate the command *)
aspinall@15146
   806
    val sync = OuterSyntax.scan "\\<^sync>";
aspinall@15146
   807
wenzelm@16534
   808
    fun named_item_elt_with nameattr toks str elt nameP objtyp =
wenzelm@16534
   809
        let
wenzelm@16534
   810
            val name = (fst (nameP (toks@sync)))
wenzelm@16534
   811
                        handle _ => (error ("Error occurred in name parser for " ^ elt ^
wenzelm@16534
   812
                                            "(objtype: " ^ objtyp ^ ")");
wenzelm@16534
   813
                                     "")
wenzelm@16534
   814
wenzelm@16534
   815
        in
wenzelm@16534
   816
            [XML.element elt
wenzelm@16534
   817
                         ((if name="" then [] else [(nameattr, name)])@
wenzelm@16534
   818
                          (if objtyp="" then [] else [("objtype", objtyp)]))
wenzelm@16534
   819
                         ([XML.text str])]
wenzelm@16534
   820
        end
aspinall@15145
   821
aspinall@15146
   822
    val named_item_elt = named_item_elt_with "name"
aspinall@15146
   823
    val thmnamed_item_elt = named_item_elt_with "thmname"
wenzelm@16534
   824
aspinall@15145
   825
    fun parse_warning msg = warning ("script->PGIP markup parser: " ^ msg)
aspinall@15145
   826
aspinall@15145
   827
    (* FIXME: allow dynamic extensions to language here: we need a hook in
aspinall@15145
   828
       outer_syntax.ML to reset this table. *)
aspinall@15145
   829
wenzelm@16534
   830
    val keywords_classification_table = ref (NONE: string Symtab.table option)
aspinall@15145
   831
wenzelm@16534
   832
    fun get_keywords_classification_table () =
wenzelm@16534
   833
        case (!keywords_classification_table) of
wenzelm@17221
   834
          SOME t => t
wenzelm@17221
   835
        | NONE => (let
wenzelm@17417
   836
                     val tab = fold (fn (c, _, k, _) => Symtab.update (c, k))
wenzelm@17221
   837
                                    (OuterSyntax.dest_parsers ()) Symtab.empty;
wenzelm@17221
   838
                   in (keywords_classification_table := SOME tab; tab) end)
aspinall@15145
   839
aspinall@15145
   840
wenzelm@16534
   841
aspinall@15145
   842
    fun xmls_of_thy_begin (name,toks,str) = (* see isar_syn.ML/theoryP *)
wenzelm@16534
   843
        let
wenzelm@16534
   844
            val ((thyname,imports,files),_) = ThyHeader.args (toks@sync)
wenzelm@16534
   845
        in
wenzelm@16534
   846
            markup_text_attrs str "opentheory"
wenzelm@16534
   847
                              ([("thyname",thyname)] @
wenzelm@16534
   848
                               (if imports=[] then [] else
wenzelm@16534
   849
                                [("parentnames", (space_implode ";" imports) ^ ";")]))
wenzelm@16534
   850
        end
aspinall@15145
   851
aspinall@15145
   852
    fun xmls_of_thy_decl (name,toks,str) = (* see isar_syn.ML/thy_decl cases  *)
wenzelm@16534
   853
        let
wenzelm@16534
   854
            (* NB: PGIP only deals with single name bindings at the moment;
wenzelm@16534
   855
               potentially we could markup grouped definitions several times but
wenzelm@16534
   856
               that might suggest the wrong structure to the editor?
wenzelm@16534
   857
               Better alternative would be to put naming closer around text,
wenzelm@16534
   858
               but to do that we'd be much better off modifying the real parser
wenzelm@16534
   859
               instead of reconstructing it here. *)
aspinall@15134
   860
wenzelm@16534
   861
            val plain_items = (* no names, unimportant names, or too difficult *)
wenzelm@16534
   862
                ["defaultsort","arities","judgement","finalconsts",
wenzelm@16534
   863
                 "syntax", "nonterminals", "translations",
wenzelm@16534
   864
                 "global", "local", "hide",
wenzelm@16534
   865
                 "ML_setup", "setup", "method_setup",
wenzelm@16534
   866
                 "parse_ast_translation", "parse_translation", "print_translation",
wenzelm@16534
   867
                 "typed_print_translation", "print_ast_translation", "token_translation",
wenzelm@16534
   868
                 "oracle",
wenzelm@16534
   869
                 "declare"]
aspinall@15145
   870
wenzelm@16534
   871
            val plain_item   = markup_text str "theoryitem"
aspinall@21472
   872
            val comment_item = markup_text str "doccomment"
wenzelm@16534
   873
            val named_item   = named_item_elt toks str "theoryitem"
aspinall@15145
   874
wenzelm@16534
   875
            val opt_overloaded = P.opt_keyword "overloaded";
aspinall@15145
   876
wenzelm@16534
   877
            val thmnameP = (* see isar_syn.ML/theoremsP *)
wenzelm@16534
   878
                let
wenzelm@16534
   879
                    val name_facts = P.and_list1 ((P.opt_thm_name "=" --| P.xthms1) >> #1)
wenzelm@16958
   880
                    val theoremsP = P.opt_locale_target |-- name_facts >> (fn [] => "" | x::_ => x)
wenzelm@16534
   881
                in
wenzelm@16534
   882
                    theoremsP
wenzelm@16534
   883
                end
wenzelm@16534
   884
        in
wenzelm@16534
   885
            (* TODO: ideally we would like to render terms properly, just as they are
wenzelm@16534
   886
               in output. This implies using PGML for symbols and variables/atoms.
wenzelm@16534
   887
               BUT it's rather tricky without having the correct concrete syntax to hand,
wenzelm@16534
   888
               and even if we did, we'd have to mess around here a whole lot more first
wenzelm@16534
   889
               to pick out the terms from the syntax. *)
aspinall@15254
   890
wenzelm@20664
   891
            if member (op =) plain_items name then plain_item
wenzelm@16534
   892
            else case name of
wenzelm@16534
   893
                     "text"      => comment_item
wenzelm@16534
   894
                   | "text_raw"  => comment_item
wenzelm@16534
   895
                   | "typedecl"  => named_item (P.type_args |-- P.name) "type"
wenzelm@16534
   896
                   | "types"     => named_item (P.type_args |-- P.name) "type"
wenzelm@16534
   897
                   | "classes"   => named_item P.name "class"
wenzelm@16534
   898
                   | "classrel"  => named_item P.name "class"
wenzelm@16534
   899
                   | "consts"    => named_item (P.const >> #1) "term"
wenzelm@16534
   900
                   | "axioms"    => named_item (P.spec_name >> (#1 o #1)) "theorem"
wenzelm@16534
   901
                   | "defs"      => named_item (opt_overloaded |-- P.spec_name >> (#1 o #1)) "theorem"
wenzelm@16534
   902
                   | "constdefs" => named_item P.name (* FIXME: heavily simplified/wrong *) "term"
wenzelm@16534
   903
                   | "theorems"  => named_item thmnameP "thmset"
wenzelm@16534
   904
                   | "lemmas"    => named_item thmnameP "thmset"
wenzelm@16534
   905
                   | "oracle"    => named_item P.name "oracle"
wenzelm@16534
   906
                   | "locale"    => named_item ((P.opt_keyword "open" >> not) |-- P.name) "locale"
wenzelm@16534
   907
                   | _ => (parse_warning ("Unrecognized thy-decl command: " ^ name); plain_item)
wenzelm@16534
   908
        end
aspinall@15145
   909
wenzelm@16534
   910
    fun xmls_of_thy_goal (name,toks,str) =
wenzelm@16534
   911
        let
wenzelm@16534
   912
            (* see isar_syn.ML/gen_theorem *)
aspinall@15146
   913
         val statement = P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.propp);
wenzelm@16534
   914
         val general_statement =
wenzelm@18130
   915
            statement >> pair [] || Scan.repeat P.locale_element -- (P.$$$ "shows" |-- statement);
wenzelm@16534
   916
wenzelm@16534
   917
            val gen_theoremP =
wenzelm@16958
   918
                P.opt_locale_target -- Scan.optional (P.opt_thm_name ":" --|
aspinall@15146
   919
                 Scan.ahead (P.locale_keyword || P.$$$ "shows")) ("", []) --
wenzelm@16534
   920
                                 general_statement >> (fn ((locale, a), (elems, concl)) =>
wenzelm@16534
   921
                                                         fst a) (* a : (bstring * Args.src list) *)
aspinall@15146
   922
wenzelm@16958
   923
            val nameP = P.opt_locale_target |-- (Scan.optional ((P.opt_thm_name ":") >> #1) "")
wenzelm@16534
   924
            (* TODO: add preference values for attributes
wenzelm@16534
   925
               val prefval = XML.element "prefval" [("name","thm-kind"),("value",name)]
wenzelm@16534
   926
            *)
wenzelm@16534
   927
        in
wenzelm@16534
   928
            (thmnamed_item_elt toks str "opengoal" nameP "") @
wenzelm@16534
   929
            (empty "openblock")
wenzelm@16534
   930
        end
aspinall@15134
   931
wenzelm@17217
   932
    fun xmls_of_qed (name,markup) =
wenzelm@17217
   933
        let val qedmarkup  =
wenzelm@17217
   934
                (case name of
wenzelm@17217
   935
                     "sorry" => markup "postponegoal"
wenzelm@17217
   936
                   | "oops"  => markup "giveupgoal"
wenzelm@17217
   937
                   | "done"  => markup "closegoal"
wenzelm@17217
   938
                   | "by"    => markup "closegoal"  (* nested or toplevel *)
wenzelm@17217
   939
                   | "qed"   => markup "closegoal"  (* nested or toplevel *)
wenzelm@17217
   940
                   | "."     => markup "closegoal"  (* nested or toplevel *)
wenzelm@17217
   941
                   | ".."    => markup "closegoal"  (* nested or toplevel *)
wenzelm@17217
   942
                   | other => (* default to closegoal: may be wrong for extns *)
wenzelm@17217
   943
                                  (parse_warning
wenzelm@17217
   944
                                       ("Unrecognized qed command: " ^ quote other);
wenzelm@17217
   945
                                       markup "closegoal"))
wenzelm@17217
   946
        in qedmarkup @ (empty "closeblock") end
aspinall@15145
   947
wenzelm@16534
   948
    fun xmls_of_kind kind (name,toks,str) =
wenzelm@16534
   949
    let val markup = markup_text str in
aspinall@15145
   950
    case kind of
aspinall@15145
   951
      "control"        => markup "badcmd"
aspinall@15145
   952
    | "diag"           => markup "spuriouscmd"
aspinall@15145
   953
    (* theory/files *)
aspinall@15145
   954
    | "theory-begin"   => xmls_of_thy_begin (name,toks,str)
aspinall@15145
   955
    | "theory-decl"    => xmls_of_thy_decl (name,toks,str)
aspinall@21472
   956
    | "theory-heading" => markup "doccomment"
aspinall@15145
   957
    | "theory-script"  => markup "theorystep"
aspinall@15146
   958
    | "theory-end"     => markup "closetheory"
aspinall@15145
   959
    (* proof control *)
aspinall@15145
   960
    | "theory-goal"    => xmls_of_thy_goal (name,toks,str)
aspinall@21472
   961
    | "proof-heading"  => markup "doccomment"
aspinall@15225
   962
    | "proof-goal"     => (markup "opengoal") @ (empty "openblock")  (* nested proof: have, show, ... *)
aspinall@15145
   963
    | "proof-block"    => markup "proofstep" (* context-shift: proof, next; really "newgoal" *)
aspinall@15145
   964
    | "proof-open"     => (empty "openblock") @ (markup "proofstep")
aspinall@15145
   965
    | "proof-close"    => (markup "proofstep") @ (empty "closeblock")
aspinall@15145
   966
    | "proof-script"   => markup "proofstep"
aspinall@15145
   967
    | "proof-chain"    => markup "proofstep"
aspinall@15145
   968
    | "proof-decl"     => markup "proofstep"
aspinall@15145
   969
    | "proof-asm"      => markup "proofstep"
aspinall@15289
   970
    | "proof-asm-goal" => (markup "opengoal") @ (empty "openblock")  (* nested proof: obtain *)
aspinall@15145
   971
    | "qed"            => xmls_of_qed (name,markup)
aspinall@15145
   972
    | "qed-block"      => xmls_of_qed (name,markup)
aspinall@15145
   973
    | "qed-global"     => xmls_of_qed (name,markup)
aspinall@15145
   974
    | other => (* default for anything else is "spuriouscmd", ignored for undo. *)
aspinall@15145
   975
      (parse_warning ("Internal inconsistency, unrecognized keyword kind: " ^ quote other);
aspinall@15145
   976
       markup "spuriouscmd")
wenzelm@16534
   977
    end
aspinall@15134
   978
in
aspinall@15145
   979
wenzelm@16534
   980
fun xmls_of_transition (name,str,toks) =
wenzelm@16534
   981
   let
wenzelm@17417
   982
     val classification = Symtab.lookup (get_keywords_classification_table ()) name
aspinall@15145
   983
   in case classification of
wenzelm@16534
   984
          SOME k => (xmls_of_kind k (name,toks,str))
wenzelm@16534
   985
        | NONE => (* an uncategorized keyword ignored for undo (maybe wrong) *)
wenzelm@16534
   986
          (parse_warning ("Uncategorized command found: " ^ name ^ " -- using spuriouscmd");
wenzelm@16534
   987
           markup_text str "spuriouscmd")
wenzelm@16534
   988
   end
aspinall@15145
   989
aspinall@15191
   990
fun markup_toks [] _ = []
aspinall@15191
   991
  | markup_toks toks x = markup_text (implode (map OuterLex.unparse toks)) x
aspinall@15191
   992
aspinall@15191
   993
fun markup_comment_whs [] = []
aspinall@15191
   994
  | markup_comment_whs (toks as t::ts) = (* this would be a lot neater if we could match on toks! *)
wenzelm@16534
   995
    let
wenzelm@16534
   996
        val (prewhs,rest) = take_prefix (OuterLex.is_kind OuterLex.Space) toks
wenzelm@16534
   997
    in
wenzelm@16534
   998
        if (prewhs <> []) then
wenzelm@16534
   999
            whitespace (implode (map OuterLex.unparse prewhs))
wenzelm@16534
  1000
            :: (markup_comment_whs rest)
wenzelm@16534
  1001
        else
wenzelm@16534
  1002
            (markup_text (OuterLex.unparse t) "comment") @
wenzelm@16534
  1003
            (markup_comment_whs ts)
aspinall@15191
  1004
    end
aspinall@15191
  1005
aspinall@15191
  1006
fun xmls_pre_cmd [] = ([],[])
wenzelm@16534
  1007
  | xmls_pre_cmd toks =
wenzelm@16534
  1008
    let
wenzelm@16534
  1009
        (* an extra token is needed to terminate the command *)
wenzelm@16534
  1010
        val sync = OuterSyntax.scan "\\<^sync>";
wenzelm@16534
  1011
        val spaceP = Scan.bulk (Scan.one (fn t =>not (OuterLex.is_proper t)) >> OuterLex.val_of) >> implode
wenzelm@16534
  1012
        val text_with_whs =
wenzelm@16534
  1013
            ((spaceP || Scan.succeed "") --
wenzelm@16534
  1014
             (P.short_ident || P.long_ident || P.sym_ident || P.string || P.number || P.verbatim) >> op^)
wenzelm@16534
  1015
             -- (spaceP || Scan.succeed "") >> op^
wenzelm@16534
  1016
        val (prewhs,rest1) = take_prefix (not o OuterLex.is_proper) (toks@sync)
aspinall@15191
  1017
        (* NB: this collapses  litcomment,(litcomment|whitespace)* to a single litcomment *)
wenzelm@16534
  1018
        val (_,rest2) = (Scan.bulk (P.$$$ "--" |-- text_with_whs) >> implode || Scan.succeed "") rest1
wenzelm@16534
  1019
        val (postwhs,rest3) = take_prefix (not o OuterLex.is_proper) rest2
aspinall@15145
  1020
    in
wenzelm@16534
  1021
        ((markup_comment_whs prewhs) @
wenzelm@16534
  1022
         (if (length rest2 = length rest1)  then []
wenzelm@16534
  1023
          else markup_text (implode
wenzelm@16534
  1024
                                (map OuterLex.unparse (Library.take (length rest1 - length rest2, rest1))))
aspinall@21472
  1025
               "doccomment") @
wenzelm@16534
  1026
         (markup_comment_whs postwhs),
wenzelm@16534
  1027
         Library.take (length rest3 - 1,rest3))
aspinall@15191
  1028
    end
aspinall@15191
  1029
wenzelm@16534
  1030
fun xmls_of_impropers toks =
wenzelm@16534
  1031
    let
wenzelm@16534
  1032
        val (xmls,rest) = xmls_pre_cmd toks
aspinall@15191
  1033
    in
wenzelm@16534
  1034
        xmls @ (markup_toks rest "unparseable")
aspinall@15145
  1035
    end
wenzelm@16534
  1036
wenzelm@16534
  1037
fun markup_unparseable str = markup_text str "unparseable"
aspinall@15173
  1038
aspinall@15145
  1039
end
aspinall@15145
  1040
aspinall@15145
  1041
aspinall@15145
  1042
local
wenzelm@16534
  1043
    (* we have to weave together the whitespace/comments with proper tokens
aspinall@15145
  1044
       to reconstruct the input. *)
aspinall@15191
  1045
    (* TODO: see if duplicating isar_output/parse_thy can help here *)
aspinall@15134
  1046
aspinall@15145
  1047
    fun match_tokens ([],us,vs) = (rev vs,us)  (* used, unused *)
wenzelm@16534
  1048
      | match_tokens (t::ts,w::ws,vs) =
wenzelm@16534
  1049
        if (t = w) then match_tokens (ts,ws,w::vs)
wenzelm@16534
  1050
        else match_tokens (t::ts,ws,w::vs)
aspinall@15145
  1051
      | match_tokens _ = error ("match_tokens: mismatched input parse")
aspinall@15145
  1052
in
aspinall@15145
  1053
    fun xmls_of_str str =
wenzelm@16534
  1054
    let
aspinall@15145
  1055
       (* parsing:   See outer_syntax.ML/toplevel_source *)
aspinall@15145
  1056
       fun parse_loop ([],[],xmls) = xmls
wenzelm@16534
  1057
         | parse_loop ([],itoks,xmls) = xmls @ (xmls_of_impropers itoks)
wenzelm@16534
  1058
         | parse_loop ((nm,toks,_)::trs,itoks,xmls) =
wenzelm@16534
  1059
           let
wenzelm@16534
  1060
               (* first proper token after whitespace/litcomment/whitespace is command *)
wenzelm@16534
  1061
               val (xmls_pre_cmd,cmditoks') = xmls_pre_cmd itoks
wenzelm@16534
  1062
               val (cmdtok,itoks') = case cmditoks' of x::xs => (x,xs)
wenzelm@16534
  1063
                                                     | _ => error("proof_general/parse_loop impossible")
wenzelm@16534
  1064
               val (utoks,itoks'') = match_tokens (toks,itoks',[])
aspinall@15145
  1065
               (* FIXME: should take trailing [w/s+] semicolon too in utoks *)
aspinall@15145
  1066
wenzelm@16534
  1067
               val str = implode (map OuterLex.unparse (cmdtok::utoks))
aspinall@15145
  1068
wenzelm@16534
  1069
               val xmls_tr  = xmls_of_transition (nm,str,toks)
wenzelm@16534
  1070
           in
wenzelm@16534
  1071
               parse_loop(trs,itoks'',xmls @ xmls_pre_cmd @ xmls_tr)
wenzelm@16534
  1072
           end
aspinall@15134
  1073
    in
wenzelm@16534
  1074
        (let val toks = OuterSyntax.scan str
wenzelm@16534
  1075
         in
wenzelm@16534
  1076
             parse_loop (OuterSyntax.read toks, toks, [])
wenzelm@16534
  1077
         end)
wenzelm@16534
  1078
           handle _ => markup_unparseable str
aspinall@15134
  1079
    end
aspinall@15134
  1080
aspinall@15134
  1081
wenzelm@16534
  1082
fun parsescript str attrs =
wenzelm@16534
  1083
    let
wenzelm@16534
  1084
        val _ = start_delay_msgs ()  (* accumulate error messages to put inside parseresult *)
wenzelm@16534
  1085
        val xmls = xmls_of_str str
aspinall@15173
  1086
        val errs = end_delayed_msgs ()
wenzelm@16534
  1087
     in
wenzelm@16534
  1088
        issue_pgips [XML.element "parseresult" attrs (errs@xmls)]
aspinall@15173
  1089
    end
aspinall@15134
  1090
end
aspinall@15134
  1091
aspinall@15134
  1092
aspinall@15134
  1093
aspinall@15134
  1094
(**** PGIP:  Isabelle -> Interface ****)
aspinall@15134
  1095
wenzelm@16534
  1096
val isabelle_pgml_version_supported = "1.0";
aspinall@15145
  1097
val isabelle_pgip_version_supported = "2.0"
aspinall@15134
  1098
aspinall@16798
  1099
(* TODO: would be cleaner to define a datatype here for the accepted elements,
aspinall@16798
  1100
   and mapping functions to/from strings.  At the moment this list must
aspinall@16798
  1101
   coincide with the strings in the function process_pgip_element. *)
wenzelm@17217
  1102
val isabelle_acceptedpgipelems =
aspinall@16798
  1103
    ["askpgip","askpgml","askprefs","getpref","setpref",
aspinall@16798
  1104
     "proverinit","proverexit","startquiet","stopquiet",
aspinall@16798
  1105
     "pgmlsymbolson", "pgmlsymbolsoff",
aspinall@16798
  1106
     "dostep", "undostep", "redostep", "abortgoal", "forget", "restoregoal",
aspinall@16798
  1107
     "askids", "showid", "askguise",
aspinall@16798
  1108
     "parsescript",
aspinall@16798
  1109
     "showproofstate", "showctxt", "searchtheorems", "setlinewidth", "viewdoc",
aspinall@16798
  1110
     "doitem", "undoitem", "redoitem", "abortheory",
aspinall@16798
  1111
     "retracttheory", "loadfile", "openfile", "closefile",
aspinall@21485
  1112
     "abortfile", "retractfile", "changecwd", "systemcmd"];
aspinall@16798
  1113
wenzelm@16534
  1114
fun usespgip () =
wenzelm@17217
  1115
    issue_pgip
wenzelm@17217
  1116
        "usespgip"
wenzelm@17217
  1117
        [("version", isabelle_pgip_version_supported)]
wenzelm@17217
  1118
        (XML.element "acceptedpgipelems" []
wenzelm@17217
  1119
                     (map (fn s=>XML.element "pgipelem"
wenzelm@17217
  1120
                                             [] (* if threads: possibility to add async here *)
wenzelm@17217
  1121
                                             [s])
wenzelm@17217
  1122
                          isabelle_acceptedpgipelems))
aspinall@15134
  1123
wenzelm@16534
  1124
fun usespgml () =
aspinall@16798
  1125
    issue_pgipe "usespgml" [("version", isabelle_pgml_version_supported)]
aspinall@15134
  1126
wenzelm@16534
  1127
fun hasprefs () =
skalberg@15570
  1128
    List.app (fn (prefcat, prefs) =>
wenzelm@16534
  1129
            issue_pgips [XML.element "hasprefs" [("prefcategory",prefcat)]
wenzelm@16534
  1130
                 (map (fn (name, (descr, (ty, (default,_),_))) =>
wenzelm@16534
  1131
                       XML.element "haspref" [("name", name),
wenzelm@16534
  1132
                                              ("descr", descr),
wenzelm@16534
  1133
                                              ("default", default)]
aspinall@16798
  1134
                       [ty]) prefs)]) (!preferences)
aspinall@15134
  1135
wenzelm@19473
  1136
fun allprefs () = maps snd (!preferences)
wenzelm@16534
  1137
wenzelm@16534
  1138
fun setpref name value =
haftmann@17314
  1139
    (case AList.lookup (op =) (allprefs ()) name of
wenzelm@16534
  1140
         NONE => warning ("Unknown pref: " ^ quote name)
skalberg@15531
  1141
       | SOME (_, (_, _, set)) => set value);
aspinall@15134
  1142
wenzelm@16534
  1143
fun getpref name =
haftmann@17314
  1144
    (case AList.lookup (op =) (allprefs ()) name of
wenzelm@16534
  1145
         NONE => warning ("Unknown pref: " ^ quote name)
wenzelm@16534
  1146
       | SOME (_, (_, (_,get), _)) =>
wenzelm@16534
  1147
           issue_pgip "prefval" [("name", name)] (get ()));
aspinall@15134
  1148
aspinall@15134
  1149
aspinall@15134
  1150
aspinall@21464
  1151
aspinall@15134
  1152
(**** PGIP:  Interface -> Isabelle/Isar ****)
aspinall@15134
  1153
aspinall@15134
  1154
exception PGIP of string;
aspinall@15134
  1155
exception PGIP_QUIT;
aspinall@15134
  1156
wenzelm@16534
  1157
aspinall@15134
  1158
(* Sending commands to Isar *)
aspinall@15134
  1159
wenzelm@16534
  1160
fun isarcmd s =
wenzelm@16534
  1161
    s |> OuterSyntax.scan |> OuterSyntax.read
aspinall@15145
  1162
      |> map (Toplevel.position (Position.name "PGIP message") o #3) |> Toplevel.>>>;
aspinall@15134
  1163
aspinall@15145
  1164
fun xmltext ((XML.Text text)::ts) = text ^ (xmltext ts)
aspinall@15145
  1165
  | xmltext [] = ""
aspinall@15145
  1166
  | xmltext _ = raise PGIP "Expected text (PCDATA/CDATA)"
wenzelm@16534
  1167
aspinall@15145
  1168
fun isarscript xmls = isarcmd (xmltext xmls)   (* send a script command *)
aspinall@15134
  1169
aspinall@15134
  1170
aspinall@16791
  1171
(* load an arbitrary file (must be .thy or .ML) *)
aspinall@15134
  1172
wenzelm@16534
  1173
fun use_thy_or_ml_file file =
aspinall@15134
  1174
    let
wenzelm@16534
  1175
        val (path,extn) = Path.split_ext (Path.unpack file)
aspinall@15134
  1176
    in
wenzelm@16534
  1177
        case extn of
wenzelm@16534
  1178
            "" => isarcmd ("use_thy " ^ (quote (Path.pack path)))
wenzelm@16534
  1179
          | "thy" => isarcmd ("use_thy " ^ (quote (Path.pack path)))
wenzelm@16534
  1180
          | "ML" => isarcmd ("use " ^ quote file)
wenzelm@16534
  1181
          | other => error ("Don't know how to read a file with extension " ^ other)
wenzelm@16534
  1182
    end
aspinall@15134
  1183
aspinall@15134
  1184
aspinall@15173
  1185
(* Proof control commands *)
aspinall@15134
  1186
aspinall@15173
  1187
local
haftmann@17314
  1188
  fun xmlattro attr attrs = AList.lookup (op =) attrs attr
aspinall@15134
  1189
wenzelm@16534
  1190
  fun xmlattr attr attrs =
wenzelm@16534
  1191
      (case xmlattro attr attrs of
wenzelm@16534
  1192
           SOME value => value
wenzelm@16534
  1193
         | NONE => raise PGIP ("Missing attribute: " ^ attr))
aspinall@15134
  1194
aspinall@15173
  1195
  val thyname_attro = xmlattro "thyname"
aspinall@15173
  1196
  val thyname_attr = xmlattr "thyname"
aspinall@15173
  1197
  val objtype_attro = xmlattro "objtype"
aspinall@15173
  1198
  val objtype_attr = xmlattr "objtype"
aspinall@15173
  1199
  val name_attr = xmlattr "name"
aspinall@15173
  1200
  val dirname_attr = xmlattr "dir"
aspinall@15134
  1201
  fun comment x = "(* " ^ x ^ " *)"
aspinall@15134
  1202
aspinall@15173
  1203
  fun localfile_of_url url = (* only handle file:/// or file://localhost/ *)
aspinall@15173
  1204
      case Url.unpack url of
wenzelm@16534
  1205
          (Url.File path) => File.platform_path path
wenzelm@16534
  1206
        | _ => error ("Cannot access non-local URL " ^ url)
aspinall@15134
  1207
aspinall@15173
  1208
  val fileurl_of = localfile_of_url o (xmlattr "url")
aspinall@15134
  1209
aspinall@15134
  1210
  val topthy = Toplevel.theory_of o Toplevel.get_state
wenzelm@16440
  1211
  val topthy_name = Context.theory_name o topthy
aspinall@15134
  1212
skalberg@15531
  1213
  val currently_open_file = ref (NONE : string option)
aspinall@15629
  1214
aspinall@16791
  1215
  (* Path management: we allow theory files to have dependencies
aspinall@16791
  1216
     in their own directory, but when we change directory for a new
aspinall@16791
  1217
     file we remove the path.  Leaving it there can cause confusion
aspinall@16791
  1218
     with difference in batch mode.a  NB: PGIP does not assume
aspinall@16791
  1219
     that the prover has a load path. *)
wenzelm@17217
  1220
  local
aspinall@16791
  1221
      val current_working_dir = ref (NONE : string option)
aspinall@16791
  1222
  in
wenzelm@17217
  1223
      fun changecwd dir =
wenzelm@17217
  1224
          (case (!current_working_dir) of
wenzelm@17217
  1225
               NONE => ()
aspinall@16791
  1226
             | SOME dir => ThyLoad.del_path dir;
wenzelm@17217
  1227
           ThyLoad.add_path dir;
wenzelm@17217
  1228
           current_working_dir := SOME dir)
aspinall@16791
  1229
  end
aspinall@16791
  1230
wenzelm@18587
  1231
  fun topproofpos () = try Toplevel.proof_position_of (Isar.state ());
aspinall@15134
  1232
in
aspinall@15134
  1233
wenzelm@16534
  1234
fun process_pgip_element pgipxml = (case pgipxml of
aspinall@15145
  1235
  (XML.Text t) => warning ("Ignored text in PGIP packet: \n" ^ t)
wenzelm@16534
  1236
| (xml as (XML.Elem (elem, attrs, data))) =>
aspinall@15145
  1237
  (case elem of
aspinall@15145
  1238
       (* protocol config *)
wenzelm@16534
  1239
       "askpgip"        => (pgip_emacs_compatibility_flag:=false; (* PG>=3.6 or other PGIP interface *)
wenzelm@16534
  1240
                            usespgip (); send_pgip_config ())
wenzelm@16534
  1241
     | "askpgml"        => usespgml ()
aspinall@15145
  1242
     (* proverconfig *)
wenzelm@16534
  1243
     | "askprefs"       => hasprefs ()
wenzelm@16534
  1244
     | "getpref"        => getpref (name_attr attrs)
wenzelm@16534
  1245
     | "setpref"        => setpref (name_attr attrs) (xmltext data)
aspinall@15145
  1246
     (* provercontrol *)
wenzelm@16534
  1247
     | "proverinit"     => isar_restart ()
wenzelm@16534
  1248
     | "proverexit"     => isarcmd "quit"
wenzelm@16534
  1249
     | "startquiet"     => isarcmd "disable_pr"
wenzelm@16534
  1250
     | "stopquiet"      => isarcmd "enable_pr"
wenzelm@18174
  1251
     | "pgmlsymbolson"   => change print_mode (fn mode =>
wenzelm@18174
  1252
          remove (op =) Symbol.xsymbolsN mode @ [Symbol.xsymbolsN])
wenzelm@17217
  1253
     | "pgmlsymbolsoff"  => change print_mode (remove (op =) Symbol.xsymbolsN)
aspinall@15145
  1254
     (* properproofcmd: proper commands which belong in script *)
aspinall@15401
  1255
     (* FIXME: next ten are by Eclipse interface, can be removed in favour of dostep *)
aspinall@15629
  1256
     (* NB: Isar doesn't make lemma name of goal accessible during proof *)
aspinall@15145
  1257
     | "opengoal"       => isarscript data
aspinall@15145
  1258
     | "proofstep"      => isarscript data
aspinall@15145
  1259
     | "closegoal"      => isarscript data
aspinall@15145
  1260
     | "giveupgoal"     => isarscript data
aspinall@15145
  1261
     | "postponegoal"   => isarscript data
aspinall@21472
  1262
     | "comment"        => isarscript data  
aspinall@21472
  1263
     | "doccomment"     => isarscript data  
wenzelm@16534
  1264
     | "whitespace"     => isarscript data  (* NB: should be ignored, but process anyway *)
aspinall@21472
  1265
     | "litcomment"     => isarscript data  (* NB: should be ignored, process for back compat *)
aspinall@15145
  1266
     | "spuriouscmd"    => isarscript data
wenzelm@16534
  1267
     | "badcmd"         => isarscript data
aspinall@15145
  1268
     (* improperproofcmd: improper commands which *do not* belong in script *)
aspinall@15401
  1269
     | "dostep"         => isarscript data
aspinall@15286
  1270
     | "undostep"       => isarcmd "undos_proof 1"
aspinall@15626
  1271
     | "redostep"       => isarcmd "redo"
wenzelm@16534
  1272
     | "abortgoal"      => isarcmd "ProofGeneral.kill_proof"
wenzelm@16534
  1273
     | "forget"         => error "Not implemented"
aspinall@15145
  1274
     | "restoregoal"    => error "Not implemented"  (* could just treat as forget? *)
aspinall@15145
  1275
     (* proofctxt: improper commands *)
aspinall@15173
  1276
     | "askids"         => askids (thyname_attro attrs, objtype_attro attrs)
wenzelm@16534
  1277
     | "showid"         => showid (thyname_attro attrs, objtype_attr attrs, name_attr attrs)
wenzelm@16534
  1278
     | "askguise"       => send_informguise (!currently_open_file,
wenzelm@16534
  1279
                                             SOME (topthy_name()) handle Toplevel.UNDEF => NONE,
wenzelm@16534
  1280
                                             topproofpos())
aspinall@15173
  1281
     | "parsescript"    => parsescript (xmltext data) attrs (* just pass back attrs unchanged *)
aspinall@15145
  1282
     | "showproofstate" => isarcmd "pr"
aspinall@15145
  1283
     | "showctxt"       => isarcmd "print_theory"   (* more useful than print_context *)
wenzelm@17217
  1284
     | "searchtheorems" => isarcmd ("thms_containing " ^ xmltext data)
wenzelm@17217
  1285
     | "setlinewidth"   => isarcmd ("pretty_setmargin " ^ xmltext data)
wenzelm@17217
  1286
     | "viewdoc"        => isarcmd ("print_" ^ xmltext data) (* FIXME: isatool doc? *)
aspinall@15145
  1287
     (* properfilecmd: proper theory-level script commands *)
aspinall@15401
  1288
     (* FIXME: next three are sent by Eclipse, can be removed in favour of doitem *)
aspinall@15145
  1289
     | "opentheory"     => isarscript data
aspinall@15145
  1290
     | "theoryitem"     => isarscript data
wenzelm@16534
  1291
     | "closetheory"    => let
wenzelm@16534
  1292
                              val thyname = topthy_name()
wenzelm@16534
  1293
                           in (isarscript data;
wenzelm@17217
  1294
                               writeln ("Theory " ^ quote thyname ^ " completed."))
wenzelm@16534
  1295
                           end
aspinall@15145
  1296
     (* improperfilecmd: theory-level commands not in script *)
aspinall@15401
  1297
     | "doitem"         => isarscript data
aspinall@21484
  1298
     | "undoitem"       => isarcmd "ProofGeneral.undo"  (* NB: named target not supported *)
aspinall@15626
  1299
     | "redoitem"       => isarcmd "ProofGeneral.redo"
aspinall@15145
  1300
     | "aborttheory"    => isarcmd ("init_toplevel")
wenzelm@17217
  1301
     | "retracttheory"  => isarcmd ("kill_thy " ^ quote (thyname_attr attrs))
aspinall@21484
  1302
     | "loadfile"       => (case !currently_open_file of
aspinall@21484
  1303
                                SOME f => raise PGIP ("loadfile when a file is open!")
aspinall@21484
  1304
                              | NONE => use_thy_or_ml_file (fileurl_of attrs))
aspinall@21484
  1305
     | "openfile"       => (case !currently_open_file of
aspinall@21484
  1306
                                SOME f => raise PGIP ("openfile when a file is already open!")
aspinall@21484
  1307
                              | NONE => (openfile_retract (fileurl_of attrs);
aspinall@21484
  1308
					 currently_open_file := SOME (fileurl_of attrs)))
wenzelm@16534
  1309
     | "closefile"      => (case !currently_open_file of
aspinall@21562
  1310
                                SOME f => (proper_inform_file_processed f (Isar.state());
wenzelm@16534
  1311
                                           currently_open_file := NONE)
wenzelm@16534
  1312
                              | NONE => raise PGIP ("closefile when no file is open!"))
aspinall@21484
  1313
     | "abortfile"      => (case !currently_open_file of
aspinall@21484
  1314
                                SOME f => (isarcmd "init_toplevel";
aspinall@21484
  1315
					   currently_open_file := NONE)
aspinall@21484
  1316
                              | NONE => raise PGIP ("abortfile when no file is open!"))
aspinall@21484
  1317
     | "retractfile"    => (case !currently_open_file of
aspinall@21484
  1318
                                SOME f => raise PGIP ("retractfile when a file is open!")
aspinall@21484
  1319
                              | NONE => inform_file_retracted (fileurl_of attrs))
aspinall@21538
  1320
     | "changecwd"      => changecwd (fileurl_of attrs)
wenzelm@16534
  1321
     | "systemcmd"      => isarscript data
aspinall@15145
  1322
     (* unofficial command for debugging *)
wenzelm@16534
  1323
     | "quitpgip" => raise PGIP_QUIT
aspinall@15145
  1324
     | _ => raise PGIP ("Unrecognized PGIP element: " ^ elem)))
aspinall@15134
  1325
wenzelm@16534
  1326
fun process_pgip_tree xml =
aspinall@16821
  1327
    (pgip_refid := NONE;
aspinall@16821
  1328
     pgip_refseq := NONE;
aspinall@15173
  1329
     (case xml of
wenzelm@16534
  1330
          XML.Elem ("pgip", attrs, pgips) =>
wenzelm@16534
  1331
          (let
aspinall@17407
  1332
               val class = xmlattr "class" attrs
wenzelm@17217
  1333
               val dest  = xmlattro "destid" attrs
aspinall@16821
  1334
               val _ = (pgip_refid :=  xmlattro "id" attrs;
wenzelm@17217
  1335
                        pgip_refseq := xmlattro "seq" attrs)
wenzelm@16534
  1336
           in
wenzelm@17217
  1337
               (* We respond to broadcast messages to provers, or
aspinall@16821
  1338
                  messages intended uniquely for us.  Silently ignore rest. *)
aspinall@16821
  1339
               case dest of
wenzelm@17217
  1340
                   NONE => if (class = "pa") then
wenzelm@17217
  1341
                               (List.app process_pgip_element pgips; true)
wenzelm@17217
  1342
                           else false
wenzelm@17217
  1343
                 | SOME id => if (matching_pgip_id id) then
wenzelm@17217
  1344
                                  (List.app process_pgip_element pgips; true)
wenzelm@17217
  1345
                              else false
wenzelm@16534
  1346
           end)
wenzelm@16534
  1347
        | _ => raise PGIP "Invalid PGIP packet received")
wenzelm@18678
  1348
     handle PGIP msg =>
wenzelm@18678
  1349
            error (msg ^ "\nPGIP error occured in XML text below:\n" ^
wenzelm@18678
  1350
                    (XML.string_of_tree xml)))
aspinall@15134
  1351
aspinall@16821
  1352
val process_pgip = K () o process_pgip_tree o XML.tree_of_string
aspinall@15191
  1353
aspinall@15134
  1354
end
aspinall@15134
  1355
aspinall@15134
  1356
aspinall@15134
  1357
(* PGIP loop: process PGIP input only *)
aspinall@15134
  1358
wenzelm@16534
  1359
local
aspinall@15134
  1360
aspinall@15145
  1361
exception XML_PARSE
aspinall@15134
  1362
aspinall@16821
  1363
fun loop ready src =
wenzelm@16534
  1364
    let
aspinall@16821
  1365
        val _ = if ready then (issue_pgipe "ready" []) else ()
wenzelm@16534
  1366
        val pgipo = (Source.get_single src)
wenzelm@16534
  1367
                        handle e => raise XML_PARSE
aspinall@15134
  1368
    in
wenzelm@16534
  1369
        case pgipo of
wenzelm@16534
  1370
             NONE  => ()
wenzelm@16534
  1371
           | SOME (pgip,src') =>
wenzelm@17217
  1372
             let
wenzelm@17217
  1373
                 val ready' = (process_pgip_tree pgip) handle e => (handler (e,SOME src'); true)
wenzelm@17217
  1374
             in
wenzelm@17217
  1375
                 loop ready' src'
wenzelm@17217
  1376
             end
skalberg@15531
  1377
    end handle e => handler (e,SOME src)  (* i.e. error in ready/XML parse *)
aspinall@15134
  1378
wenzelm@16534
  1379
and handler (e,srco) =
aspinall@15145
  1380
    case (e,srco) of
wenzelm@16534
  1381
        (XML_PARSE,SOME src) =>
wenzelm@18678
  1382
        Output.panic "Invalid XML input, aborting" (* NB: loop OK for tty, but want exit on EOF *)
aspinall@15145
  1383
      | (PGIP_QUIT,_) => ()
aspinall@16821
  1384
      | (Interrupt,SOME src) => (!error_fn "Interrupt during PGIP processing"; loop true src)
aspinall@16821
  1385
      | (Toplevel.UNDEF,SOME src) => (error "No working context defined"; loop true src) (* usually *)
aspinall@16821
  1386
      | (e,SOME src) => (error (Toplevel.exn_message e); loop true src)
skalberg@15531
  1387
      | (_,NONE) => ()
aspinall@15134
  1388
in
aspinall@15145
  1389
  (* NB: simple tty for now; later might read from other tty-style sources (e.g. sockets). *)
aspinall@15145
  1390
aspinall@15145
  1391
  val xmlP = XML.scan_comment_whspc |-- XML.parse_elem >> single
aspinall@15145
  1392
wenzelm@20738
  1393
  val tty_src = Source.set_prompt "" (Source.source Symbol.stopper xmlP NONE Source.tty)
aspinall@15145
  1394
haftmann@16824
  1395
  fun pgip_toplevel x = loop true x
aspinall@15134
  1396
end
aspinall@15134
  1397
aspinall@15134
  1398
aspinall@15134
  1399
(* additional outer syntax for Isar *)
wenzelm@12778
  1400
wenzelm@17057
  1401
local structure P = OuterParse and K = OuterKeyword in
wenzelm@12778
  1402
wenzelm@16534
  1403
val undoP = (*undo without output*)
wenzelm@12778
  1404
  OuterSyntax.improper_command "ProofGeneral.undo" "(internal)" K.control
wenzelm@12778
  1405
    (Scan.succeed (Toplevel.no_timing o IsarCmd.undo));
wenzelm@12778
  1406
wenzelm@16534
  1407
val redoP = (*redo without output*)
aspinall@15626
  1408
  OuterSyntax.improper_command "ProofGeneral.redo" "(internal)" K.control
aspinall@15626
  1409
    (Scan.succeed (Toplevel.no_timing o IsarCmd.redo));
aspinall@15626
  1410
wenzelm@12778
  1411
val context_thy_onlyP =
wenzelm@12778
  1412
  OuterSyntax.improper_command "ProofGeneral.context_thy_only" "(internal)" K.control
wenzelm@21350
  1413
    (P.name >> (Toplevel.no_timing oo IsarCmd.init_context update_thy_only));
wenzelm@12778
  1414
wenzelm@12778
  1415
val try_context_thy_onlyP =
wenzelm@12778
  1416
  OuterSyntax.improper_command "ProofGeneral.try_context_thy_only" "(internal)" K.control
wenzelm@12778
  1417
    (P.name >> (Toplevel.no_timing oo
wenzelm@21350
  1418
      (Toplevel.imperative (K ()) oo IsarCmd.init_context try_update_thy_only)));
wenzelm@12778
  1419
wenzelm@12778
  1420
val restartP =
wenzelm@12778
  1421
  OuterSyntax.improper_command "ProofGeneral.restart" "(internal)" K.control
wenzelm@12778
  1422
    (P.opt_unit >> (Toplevel.no_timing oo K (Toplevel.imperative isar_restart)));
wenzelm@12778
  1423
wenzelm@12778
  1424
val kill_proofP =
wenzelm@12778
  1425
  OuterSyntax.improper_command "ProofGeneral.kill_proof" "(internal)" K.control
wenzelm@12778
  1426
    (Scan.succeed (Toplevel.no_timing o IsarCmd.kill_proof_notify tell_clear_goals));
wenzelm@12778
  1427
wenzelm@12778
  1428
val inform_file_processedP =
wenzelm@12778
  1429
  OuterSyntax.improper_command "ProofGeneral.inform_file_processed" "(internal)" K.control
wenzelm@14902
  1430
    (P.name >> (fn file => Toplevel.no_timing o
wenzelm@14902
  1431
      Toplevel.keep (vacuous_inform_file_processed file) o
wenzelm@14902
  1432
      Toplevel.kill o
wenzelm@14902
  1433
      Toplevel.keep (proper_inform_file_processed file)));
wenzelm@12778
  1434
wenzelm@12778
  1435
val inform_file_retractedP =
wenzelm@12778
  1436
  OuterSyntax.improper_command "ProofGeneral.inform_file_retracted" "(internal)" K.control
wenzelm@12778
  1437
    (P.name >> (Toplevel.no_timing oo
wenzelm@14902
  1438
      (fn file => Toplevel.imperative (fn () => inform_file_retracted file))));
wenzelm@12778
  1439
wenzelm@14725
  1440
val process_pgipP =
wenzelm@14725
  1441
  OuterSyntax.improper_command "ProofGeneral.process_pgip" "(internal)" K.control
wenzelm@14725
  1442
    (P.text >> (Toplevel.no_timing oo
wenzelm@14725
  1443
      (fn txt => Toplevel.imperative (fn () => process_pgip txt))));
wenzelm@14725
  1444
wenzelm@12778
  1445
fun init_outer_syntax () = OuterSyntax.add_parsers
aspinall@15626
  1446
 [undoP, redoP, restartP, kill_proofP, context_thy_onlyP, try_context_thy_onlyP,
wenzelm@14725
  1447
  inform_file_processedP, inform_file_retractedP, process_pgipP];
wenzelm@12778
  1448
wenzelm@12778
  1449
end;
wenzelm@12778
  1450
wenzelm@12778
  1451
wenzelm@12778
  1452
(* init *)
wenzelm@12778
  1453
wenzelm@12778
  1454
val initialized = ref false;
wenzelm@12778
  1455
wenzelm@16534
  1456
fun set_prompts true _ = ml_prompts "ML> " "ML# "
aspinall@15134
  1457
  | set_prompts false true = ml_prompts "PGIP-ML>" "PGIP-ML# "
wenzelm@17217
  1458
  | set_prompts false false = ml_prompts ("> " ^ special "372") ("- " ^ special "373");
aspinall@15134
  1459
aspinall@15134
  1460
fun init_setup isar pgip =
wenzelm@16534
  1461
  (conditional (not (! initialized)) (fn () =>
wenzelm@12778
  1462
   (if isar then setmp warning_fn (K ()) init_outer_syntax () else ();
wenzelm@12778
  1463
    setup_xsymbols_output ();
aspinall@15134
  1464
    setup_pgml_output ();
wenzelm@12778
  1465
    setup_messages ();
wenzelm@12778
  1466
    setup_state ();
wenzelm@12778
  1467
    setup_thy_loader ();
wenzelm@13526
  1468
    setup_present_hook ();
wenzelm@12778
  1469
    set initialized; ()));
wenzelm@12778
  1470
  sync_thy_loader ();
wenzelm@17217
  1471
  change print_mode (cons proof_generalN o remove (op =) proof_generalN);
wenzelm@18993
  1472
  init_pgip_session_id ();
wenzelm@16534
  1473
  if pgip then
wenzelm@19300
  1474
    change print_mode (append [pgmlN, pgmlatomsN] o subtract (op =) [pgmlN, pgmlatomsN])
wenzelm@16534
  1475
  else
wenzelm@16534
  1476
    pgip_emacs_compatibility_flag := true;  (* assume this for PG <3.6 compatibility *)
aspinall@15134
  1477
  set_prompts isar pgip;
wenzelm@16534
  1478
  pgip_active := pgip);
aspinall@15134
  1479
wenzelm@16534
  1480
fun init isar =
wenzelm@16534
  1481
 (init_setup isar false;
wenzelm@16534
  1482
  if isar then Isar.sync_main () else isa_restart ());
aspinall@15134
  1483
wenzelm@18678
  1484
fun init_pgip false = Output.panic "PGIP not supported for Isabelle/classic mode."
wenzelm@16534
  1485
  | init_pgip true = (init_setup true true; pgip_toplevel tty_src);
wenzelm@12778
  1486
wenzelm@12778
  1487
wenzelm@12778
  1488
wenzelm@16534
  1489
(** generate elisp file for keyword classification **)
wenzelm@12778
  1490
wenzelm@12778
  1491
local
wenzelm@12778
  1492
wenzelm@20664
  1493
val regexp_meta = member (op =) (explode ".*+?[]^$");
wenzelm@16534
  1494
val regexp_quote =
wenzelm@20664
  1495
  implode o map (fn c => if regexp_meta c then "\\\\" ^ c else c) o explode;
wenzelm@12778
  1496
wenzelm@12778
  1497
fun defconst name strs =
wenzelm@12778
  1498
  "\n(defconst isar-keywords-" ^ name ^
wenzelm@12778
  1499
  "\n  '(" ^ space_implode "\n    " (map (quote o regexp_quote) strs) ^ "))\n";
wenzelm@12778
  1500
wenzelm@16534
  1501
fun make_elisp_commands commands kind = defconst kind
wenzelm@19482
  1502
  (commands |> map_filter (fn (c, _, k, _) => if k = kind then SOME c else NONE));
wenzelm@12778
  1503
wenzelm@12778
  1504
fun make_elisp_syntax (keywords, commands) =
wenzelm@12778
  1505
  ";;\n\
wenzelm@12778
  1506
  \;; Keyword classification tables for Isabelle/Isar.\n\
wenzelm@12778
  1507
  \;; This file was generated by " ^ Session.name () ^ " -- DO NOT EDIT!\n\
wenzelm@12778
  1508
  \;;\n\
wenzelm@12778
  1509
  \;; $" ^ "Id$\n\
wenzelm@12778
  1510
  \;;\n" ^
wenzelm@12778
  1511
  defconst "major" (map #1 commands) ^
skalberg@15570
  1512
  defconst "minor" (List.filter Syntax.is_identifier keywords) ^
wenzelm@17057
  1513
  implode (map (make_elisp_commands commands) OuterKeyword.kinds) ^
wenzelm@12778
  1514
  "\n(provide 'isar-keywords)\n";
wenzelm@12778
  1515
wenzelm@12778
  1516
in
wenzelm@12778
  1517
wenzelm@12778
  1518
fun write_keywords s =
wenzelm@16534
  1519
 (init_outer_syntax ();
wenzelm@16534
  1520
  File.write (Path.unpack ("isar-keywords" ^ (if s = "" then "" else "-" ^ s) ^".el"))
wenzelm@16534
  1521
    (make_elisp_syntax (OuterSyntax.dest_keywords (), OuterSyntax.dest_parsers ())));
wenzelm@12778
  1522
wenzelm@12778
  1523
end;
wenzelm@12778
  1524
aspinall@21464
  1525
wenzelm@16534
  1526
end;