src/Pure/proof_general.ML
author aspinall
Mon Aug 16 18:05:41 2004 +0200 (2004-08-16)
changeset 15134 d3fa5e1d6e4d
parent 15010 72fbe711e414
child 15145 07360eef9f4f
permissions -rw-r--r--
Experimental version supporting PGIP, merged with main branch with help from Makarius.
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
aspinall@15134
     5
Isabelle configuration for Proof General (see http://proofgeneral.inf.ed.ac.uk)
aspinall@15134
     6
Includes support for PGIP control language for Isabelle/Isar.
aspinall@15134
     7
aspinall@15134
     8
===========================================================================
aspinall@15134
     9
NOTE: With this version you will lose support for the Isabelle
aspinall@15134
    10
preferences menu in the currently released version of Proof General (3.5).
aspinall@15134
    11
No other changes should be visible in the Emacs interface.
aspinall@15134
    12
aspinall@15134
    13
If the loss of preferences is a serious problem, please use a "sticky"
aspinall@15134
    14
check-out of the previous version of this file, version 1.27.
aspinall@15134
    15
aspinall@15134
    16
A version of Proof General which supports the new PGIP format for
aspinall@15134
    17
preferences will be available shortly.  
aspinall@15134
    18
===========================================================================
aspinall@15134
    19
aspinall@15134
    20
STATUS: this version is an interim experimental version that was
aspinall@15134
    21
used from 07.2003-08.2004 for the development of PGIP 1.X.  This will
aspinall@15134
    22
soon be replaced by a version for PGIP 2.X.
aspinall@15134
    23
wenzelm@12778
    24
*)
wenzelm@12778
    25
wenzelm@12778
    26
signature PROOF_GENERAL =
wenzelm@12778
    27
sig
wenzelm@12778
    28
  val setup: (theory -> theory) list
wenzelm@12778
    29
  val update_thy_only: string -> unit
wenzelm@12778
    30
  val try_update_thy_only: string -> unit
wenzelm@13391
    31
  val inform_file_retracted: string -> unit
wenzelm@12778
    32
  val inform_file_processed: string -> unit
aspinall@15134
    33
  val preferences: 
aspinall@15134
    34
      (string * 
aspinall@15134
    35
	(string * 
aspinall@15134
    36
	 (string * 
aspinall@15134
    37
	  (string * (string * (unit -> string)) * 
aspinall@15134
    38
	   (string -> unit)))) list) list ref
berghofe@13728
    39
  val process_pgip: string -> unit
wenzelm@12778
    40
  val thms_containing: string list -> unit
wenzelm@12778
    41
  val help: unit -> unit
wenzelm@12778
    42
  val show_context: unit -> theory
wenzelm@12778
    43
  val kill_goal: unit -> unit
wenzelm@12778
    44
  val repeat_undo: int -> unit
wenzelm@12778
    45
  val isa_restart: unit -> unit
wenzelm@12833
    46
  val full_proofs: bool -> unit
aspinall@15134
    47
  val isarcmd: string -> unit
wenzelm@12778
    48
  val init: bool -> unit
aspinall@15134
    49
  val init_pgip: bool -> unit
wenzelm@12778
    50
  val write_keywords: string -> unit
wenzelm@12778
    51
end;
wenzelm@12778
    52
aspinall@15134
    53
structure ProofGeneral : PROOF_GENERAL =
wenzelm@12778
    54
struct
wenzelm@12778
    55
aspinall@15134
    56
(* PGIP messaging mode (independent of PGML output) *)
aspinall@15134
    57
aspinall@15134
    58
val pgip_active = ref false;
aspinall@15134
    59
val pgip_emacs_compatibility_flag = ref false;
aspinall@15134
    60
aspinall@15134
    61
fun pgip () = (!pgip_active);
aspinall@15134
    62
fun pgip_emacs_compatibility () = (!pgip_emacs_compatibility_flag);
aspinall@15134
    63
aspinall@15134
    64
wenzelm@12778
    65
(* print modes *)
wenzelm@12778
    66
aspinall@15134
    67
val proof_generalN = "ProofGeneral"; (* token markup (colouring vars, etc.) *)
aspinall@15134
    68
val xsymbolsN = Symbol.xsymbolsN;    (* XSymbols symbols *)
aspinall@15134
    69
val pgmlN = "PGML";		     (* XML escapes and PGML symbol elements *)
aspinall@15134
    70
val pgmlatomsN = "PGMLatoms";	     (* variable kind decorations *)
aspinall@15134
    71
val thm_depsN = "thm_deps";	     (* meta-information about theorem deps *)
wenzelm@12778
    72
wenzelm@12778
    73
fun pgml () = pgmlN mem_string ! print_mode;
wenzelm@12778
    74
aspinall@15134
    75
(* text output: print modes for xsymbol and PGML *)
wenzelm@12778
    76
wenzelm@12778
    77
local
wenzelm@12778
    78
wenzelm@14827
    79
fun xsym_output "\\" = "\\\\"
wenzelm@14827
    80
  | xsym_output s = if Symbol.is_raw s then Symbol.decode_raw s else s;
wenzelm@14827
    81
wenzelm@12778
    82
fun xsymbols_output s =
aspinall@15134
    83
  if xsymbolsN mem_string ! print_mode andalso exists_string (equal "\\") s then
wenzelm@12778
    84
    let val syms = Symbol.explode s
wenzelm@14827
    85
    in (implode (map xsym_output syms), real (Symbol.length syms)) end
aspinall@15134
    86
  else Symbol.default_output s;
aspinall@15134
    87
aspinall@15134
    88
fun pgml_sym s =
aspinall@15134
    89
  (case Symbol.decode s of
aspinall@15134
    90
    Symbol.Char "\\" => "\\\\"
aspinall@15134
    91
  | Symbol.Char s => XML.text s
aspinall@15134
    92
  | Symbol.Sym s => XML.element "sym" [("name", s)] []
aspinall@15134
    93
  | Symbol.Ctrl s => XML.element "ctrl" [("name", s)] []
aspinall@15134
    94
  | Symbol.Raw s => s);
wenzelm@12778
    95
aspinall@15134
    96
fun pgml_output str =
aspinall@15134
    97
  let val syms = Symbol.explode str
aspinall@15134
    98
  in (implode (map pgml_sym syms), real (Symbol.length syms)) end;
aspinall@15134
    99
aspinall@15134
   100
in 
wenzelm@12778
   101
aspinall@15134
   102
fun setup_xsymbols_output () = 
aspinall@15134
   103
    Output.add_mode 
aspinall@15134
   104
	xsymbolsN 
aspinall@15134
   105
	(xsymbols_output, Symbol.default_indent, Symbol.encode_raw);
wenzelm@12778
   106
aspinall@15134
   107
fun setup_pgml_output () = 
aspinall@15134
   108
    Output.add_mode 
aspinall@15134
   109
	pgmlN
aspinall@15134
   110
	(pgml_output, Symbol.default_indent, Symbol.encode_raw);
wenzelm@12778
   111
wenzelm@12778
   112
end;
wenzelm@12778
   113
wenzelm@12778
   114
wenzelm@12778
   115
(* token translations *)
wenzelm@12778
   116
wenzelm@12778
   117
local
wenzelm@12778
   118
wenzelm@12778
   119
val end_tag = oct_char "350";
wenzelm@12778
   120
val class_tag = ("class", oct_char "351");
wenzelm@12778
   121
val tfree_tag = ("tfree", oct_char "352");
wenzelm@12778
   122
val tvar_tag = ("tvar", oct_char "353");
wenzelm@12778
   123
val free_tag = ("free", oct_char "354");
wenzelm@12778
   124
val bound_tag = ("bound", oct_char "355");
wenzelm@12778
   125
val var_tag = ("var", oct_char "356");
wenzelm@12778
   126
val skolem_tag = ("skolem", oct_char "357");
wenzelm@12778
   127
wenzelm@12778
   128
fun xml_atom kind x = XML.element "atom" [("kind", kind)] [XML.text x];
wenzelm@12778
   129
wenzelm@12778
   130
fun tagit (kind, bg_tag) x =
aspinall@15134
   131
    (if Output.has_mode pgmlatomsN then 
aspinall@15134
   132
	 xml_atom kind x
aspinall@15134
   133
     else bg_tag ^ x ^ end_tag, 
aspinall@15134
   134
     real (Symbol.length (Symbol.explode x)));
wenzelm@12778
   135
wenzelm@12778
   136
fun free_or_skolem x =
wenzelm@12778
   137
  (case try Syntax.dest_skolem x of
wenzelm@12778
   138
    None => tagit free_tag x
wenzelm@12778
   139
  | Some x' => tagit skolem_tag x');
wenzelm@12778
   140
wenzelm@12778
   141
fun var_or_skolem s =
wenzelm@12778
   142
  (case Syntax.read_var s of
wenzelm@12778
   143
    Var ((x, i), _) =>
wenzelm@12778
   144
      (case try Syntax.dest_skolem x of
wenzelm@12778
   145
        None => tagit var_tag s
wenzelm@12778
   146
      | Some x' => tagit skolem_tag (Syntax.string_of_vname (x', i)))
wenzelm@12778
   147
  | _ => tagit var_tag s);
wenzelm@12778
   148
wenzelm@12778
   149
val proof_general_trans =
wenzelm@12778
   150
 Syntax.tokentrans_mode proof_generalN
wenzelm@12778
   151
  [("class", tagit class_tag),
wenzelm@12778
   152
   ("tfree", tagit tfree_tag),
wenzelm@12778
   153
   ("tvar", tagit tvar_tag),
wenzelm@12778
   154
   ("free", free_or_skolem),
wenzelm@12778
   155
   ("bound", tagit bound_tag),
wenzelm@12778
   156
   ("var", var_or_skolem)];
wenzelm@12778
   157
wenzelm@12778
   158
in val setup = [Theory.add_tokentrfuns proof_general_trans] end;
wenzelm@12778
   159
wenzelm@12778
   160
aspinall@15134
   161
(* assembling PGIP packets *)
aspinall@15134
   162
aspinall@15134
   163
val pgip_refseq = ref None : string option ref
aspinall@15134
   164
val pgip_refid = ref None : string option ref
wenzelm@12778
   165
wenzelm@12778
   166
local
aspinall@15134
   167
    val myseq_no = ref 1;      (* PGIP packet counter *)
wenzelm@12778
   168
aspinall@15134
   169
    val pgip_class  = "pg"
aspinall@15134
   170
    val pgip_origin = "Isabelle/Isar"
aspinall@15134
   171
    val pgip_id = (getenv "HOSTNAME") ^ "/" ^ (getenv "USER") ^ "/" ^ 
aspinall@15134
   172
		   (Time.toString(Time.now()))
aspinall@15134
   173
	          (* FIXME: PPID is empty for me: any way to get process ID? *)
wenzelm@12778
   174
aspinall@15134
   175
    fun assemble_pgips pgips = 
aspinall@15134
   176
	XML.element 
aspinall@15134
   177
	     "pgip" 
aspinall@15134
   178
	     ([("class",  pgip_class),
aspinall@15134
   179
	       ("origin", pgip_origin),
aspinall@15134
   180
	       ("id",     pgip_id)] @
aspinall@15134
   181
	      (if_none (apsome (single o (pair "refseq")) (!pgip_refseq)) []) @
aspinall@15134
   182
	      (if_none (apsome (single o (pair "refid")) (!pgip_refid)) []) @
aspinall@15134
   183
	      [("seq",  string_of_int (Library.inc myseq_no))])
aspinall@15134
   184
	     pgips
wenzelm@13526
   185
in
wenzelm@12778
   186
aspinall@15134
   187
 fun decorated_output bg en prfx = 
aspinall@15134
   188
    writeln_default o enclose bg en o prefix_lines prfx;
aspinall@15134
   189
aspinall@15134
   190
 (* FIXME: see Rev 1.48 [PG CVS] for cleaner version of this which can be used
aspinall@15134
   191
    for PG 4.0 which processes PGIP without needing special chars. *)
aspinall@15134
   192
 fun issue_pgips ps = 
aspinall@15134
   193
     if pgip_emacs_compatibility() then
aspinall@15134
   194
	 decorated_output (* add urgent message annotation *)
aspinall@15134
   195
	     (oct_char "360") (oct_char "361") "" 
aspinall@15134
   196
	     (assemble_pgips ps)
aspinall@15134
   197
     else 
aspinall@15134
   198
	 writeln_default (assemble_pgips ps)
aspinall@15134
   199
aspinall@15134
   200
 fun assemble_pgip resp attrs s = assemble_pgips [XML.element resp attrs [s]]
aspinall@15134
   201
				  
aspinall@15134
   202
 fun assemble_pgipe resp attrs = assemble_pgips [XML.element resp attrs []]
aspinall@15134
   203
aspinall@15134
   204
 fun issue_pgip resp attrs = writeln_default o (assemble_pgip resp attrs)
aspinall@15134
   205
aspinall@15134
   206
(*  FIXME: temporarily to support PG 3.4.  *)
aspinall@15134
   207
 fun issue_pgip_maybe_decorated bg en resp attrs s = 
aspinall@15134
   208
     if pgip_emacs_compatibility() then
aspinall@15134
   209
      (*  in PGIP mode, but using escape characters as well.  *)
aspinall@15134
   210
	writeln_default (enclose bg en (assemble_pgip resp attrs s))
aspinall@15134
   211
     else 
aspinall@15134
   212
	issue_pgip resp attrs s
aspinall@15134
   213
	
aspinall@15134
   214
 fun issue_pgipe resp attrs = writeln_default (assemble_pgipe resp attrs)
aspinall@15134
   215
aspinall@15134
   216
end
aspinall@15134
   217
aspinall@15134
   218
(* messages and notification *)
aspinall@15134
   219
aspinall@15134
   220
fun message resp attrs bg en prfx s =
aspinall@15134
   221
  if pgip() then 
aspinall@15134
   222
      issue_pgip_maybe_decorated bg en resp attrs (prefix_lines prfx s)
aspinall@15134
   223
  else 
aspinall@15134
   224
      decorated_output bg en prfx s;
aspinall@15134
   225
aspinall@15134
   226
aspinall@15134
   227
local
aspinall@15134
   228
    val display_area = ("area", "display")
aspinall@15134
   229
    val message_area = ("area", "message")
aspinall@15134
   230
    val tracing_category = ("category", "tracing")
aspinall@15134
   231
    val urgent_indication = ("urgent", "y")
aspinall@15134
   232
    val nonfatal = ("fatality", "nonfatal")
aspinall@15134
   233
    val fatal = ("fatality", "fatal")
aspinall@15134
   234
    val panic = ("fatality", "panic")
aspinall@15134
   235
aspinall@15134
   236
    val thyname_attr = pair "thyname"
aspinall@15134
   237
    val url_attr = pair "url"
aspinall@15134
   238
    fun localfile_url_attr path = url_attr ("file:///" ^ path)
aspinall@15134
   239
in			   
wenzelm@12778
   240
wenzelm@12778
   241
fun setup_messages () =
aspinall@15134
   242
 (writeln_fn  := message "normalresponse" [message_area] "" "" "";
aspinall@15134
   243
aspinall@15134
   244
  priority_fn := message "normalresponse" [message_area, urgent_indication]
aspinall@15134
   245
			 (oct_char "360") (oct_char "361") "";
aspinall@15134
   246
aspinall@15134
   247
  tracing_fn := message "normalresponse"  [message_area, tracing_category]
aspinall@15134
   248
			(oct_char "360" ^ oct_char "375") (oct_char "361") "";
aspinall@15134
   249
aspinall@15134
   250
  warning_fn := message "errorresponse"    [nonfatal]
aspinall@15134
   251
			(oct_char "362") (oct_char "363") "### ";
aspinall@15134
   252
aspinall@15134
   253
  error_fn := message "errorresponse" [fatal]
aspinall@15134
   254
		      (oct_char "364") (oct_char "365") "*** ";
aspinall@15134
   255
aspinall@15134
   256
  panic_fn := message "errorresponse" [panic]
aspinall@15134
   257
		      (oct_char "364") (oct_char "365") "!!! ")
aspinall@15134
   258
aspinall@15134
   259
aspinall@15134
   260
(* accumulate printed output in a single PGIP response *)
aspinall@15134
   261
aspinall@15134
   262
fun with_displaywrap (elt,attrs) dispfn =
aspinall@15134
   263
    let 
aspinall@15134
   264
	val lines = ref ([] : string list);
aspinall@15134
   265
	fun wlgrablines s = (lines:= (s :: (!lines)))
aspinall@15134
   266
    in 
aspinall@15134
   267
	(setmp writeln_fn wlgrablines dispfn ();
aspinall@15134
   268
	 (* FIXME: cat_lines here inefficient, should use stream output *)
aspinall@15134
   269
         issue_pgip elt attrs (cat_lines (!lines)))
aspinall@15134
   270
    end
wenzelm@12778
   271
aspinall@15134
   272
val emacs_notify = decorated_output (oct_char "360") (oct_char "361") "";
aspinall@15134
   273
    
aspinall@15134
   274
fun tell_clear_goals () = 
aspinall@15134
   275
    if pgip() then
aspinall@15134
   276
	issue_pgipe "cleardisplay" [display_area]
aspinall@15134
   277
    else 
aspinall@15134
   278
	emacs_notify "Proof General, please clear the goals buffer.";
aspinall@15134
   279
aspinall@15134
   280
fun tell_clear_response () = 
aspinall@15134
   281
    if pgip() then
aspinall@15134
   282
	issue_pgipe "cleardisplay" [message_area]
aspinall@15134
   283
    else 
aspinall@15134
   284
	emacs_notify "Proof General, please clear the response buffer.";
wenzelm@12778
   285
aspinall@15134
   286
fun tell_file_loaded path = 
aspinall@15134
   287
    if pgip() then
aspinall@15134
   288
	issue_pgipe "informtheoryloaded"  (* FIXME: get thy name from info here? *)
aspinall@15134
   289
		    [thyname_attr        (XML.text (File.sysify_path path)),
aspinall@15134
   290
		     localfile_url_attr  (XML.text (File.sysify_path path))]
aspinall@15134
   291
    else 
aspinall@15134
   292
	emacs_notify ("Proof General, this file is loaded: " 
aspinall@15134
   293
		      ^ quote (File.sysify_path path));
aspinall@15134
   294
aspinall@15134
   295
fun tell_file_retracted path = 
aspinall@15134
   296
    if pgip() then
aspinall@15134
   297
	issue_pgipe "informtheoryretracted"  (* FIXME: get thy name from info here? *)
aspinall@15134
   298
		    [thyname_attr        (XML.text (File.sysify_path path)),
aspinall@15134
   299
		     localfile_url_attr  (XML.text (File.sysify_path path))]
aspinall@15134
   300
    else 
aspinall@15134
   301
	emacs_notify ("Proof General, you can unlock the file " 
aspinall@15134
   302
		      ^ quote (File.sysify_path path));
wenzelm@12778
   303
wenzelm@12778
   304
wenzelm@12778
   305
(* theory / proof state output *)
wenzelm@12778
   306
wenzelm@12778
   307
local
wenzelm@12778
   308
aspinall@15134
   309
    fun tmp_markers f =	setmp Display.current_goals_markers 
aspinall@15134
   310
			      (oct_char "366", oct_char "367", "") f ()
wenzelm@12778
   311
aspinall@15134
   312
    fun statedisplay prts =
aspinall@15134
   313
	issue_pgip "proofstate" []
aspinall@15134
   314
		   (XML.element "pgml" []
aspinall@15134
   315
				[XML.element "statedisplay" 
aspinall@15134
   316
					     [] 
aspinall@15134
   317
					     [Output.output (* FIXME: needed? *)
aspinall@15134
   318
						  (Pretty.output
aspinall@15134
   319
						       (Pretty.chunks prts))]])
wenzelm@13545
   320
aspinall@15134
   321
    fun print_current_goals n m st =
aspinall@15134
   322
	if pgml () then statedisplay (Display.pretty_current_goals n m st)
aspinall@15134
   323
	else tmp_markers (fn () => Display.print_current_goals_default n m st)
aspinall@15134
   324
	     
aspinall@15134
   325
    fun print_state b st =
aspinall@15134
   326
	if pgml () then statedisplay (Toplevel.pretty_state b st)
aspinall@15134
   327
	else tmp_markers (fn () => Toplevel.print_state_default b st)
wenzelm@13526
   328
in
wenzelm@13526
   329
aspinall@15134
   330
 fun setup_state () =
aspinall@15134
   331
     (Display.print_current_goals_fn := print_current_goals;
aspinall@15134
   332
      Toplevel.print_state_fn := print_state;
aspinall@15134
   333
      (* FIXME: check next octal char won't appear in pgip? *)
aspinall@15134
   334
      Toplevel.prompt_state_fn := (suffix (oct_char "372") o  
aspinall@15134
   335
				   Toplevel.prompt_state_default));
aspinall@15134
   336
end
berghofe@13728
   337
aspinall@15134
   338
end
berghofe@13728
   339
wenzelm@12778
   340
(* misc commands for ProofGeneral/isa *)
wenzelm@12778
   341
wenzelm@12778
   342
fun thms_containing ss =
wenzelm@13284
   343
  ProofContext.print_thms_containing (ProofContext.init (the_context ())) None ss;
wenzelm@12778
   344
wenzelm@12778
   345
val welcome = priority o Session.welcome;
wenzelm@12778
   346
val help = welcome;
wenzelm@12778
   347
val show_context = Context.the_context;
wenzelm@12778
   348
wenzelm@12778
   349
fun kill_goal () = (Goals.reset_goals (); tell_clear_goals ());
wenzelm@12778
   350
wenzelm@12778
   351
fun no_print_goals f = setmp Display.print_current_goals_fn (fn _ => fn _ => fn _ => ()) f;
wenzelm@12778
   352
wenzelm@12778
   353
fun repeat_undo 0 = ()
wenzelm@12778
   354
  | repeat_undo 1 = undo ()
wenzelm@12778
   355
  | repeat_undo n = (no_print_goals undo (); repeat_undo (n - 1));
wenzelm@12778
   356
wenzelm@12778
   357
aspinall@15134
   358
(* theory loader actions *)
aspinall@15134
   359
aspinall@15134
   360
local
aspinall@15134
   361
aspinall@15134
   362
fun add_master_files name files =
aspinall@15134
   363
  let val masters = [ThyLoad.thy_path name, ThyLoad.ml_path name]
aspinall@15134
   364
  in masters @ gen_rems (op = o pairself Path.base) (files, masters) end;
aspinall@15134
   365
aspinall@15134
   366
fun trace_action action name =
aspinall@15134
   367
  if action = ThyInfo.Update then
aspinall@15134
   368
    seq tell_file_loaded (ThyInfo.loaded_files name)
aspinall@15134
   369
  else if action = ThyInfo.Outdate orelse action = ThyInfo.Remove then
aspinall@15134
   370
    seq tell_file_retracted (add_master_files name (ThyInfo.loaded_files name))
aspinall@15134
   371
  else ();
aspinall@15134
   372
aspinall@15134
   373
in
aspinall@15134
   374
  fun setup_thy_loader () = ThyInfo.add_hook trace_action;
aspinall@15134
   375
  fun sync_thy_loader () = seq (trace_action ThyInfo.Update) (ThyInfo.names ());
aspinall@15134
   376
end;
aspinall@15134
   377
aspinall@15134
   378
aspinall@15134
   379
(* prepare theory context *)
aspinall@15134
   380
aspinall@15134
   381
val thy_name = Path.pack o #1 o Path.split_ext o Path.base o Path.unpack;
aspinall@15134
   382
val update_thy_only = setmp MetaSimplifier.trace_simp 
aspinall@15134
   383
			    false ThyInfo.update_thy_only;
aspinall@15134
   384
aspinall@15134
   385
fun which_context () =
aspinall@15134
   386
  (case Context.get_context () of
aspinall@15134
   387
    Some thy => "  Using current (dynamic!) one: " ^
aspinall@15134
   388
      (case try PureThy.get_name thy of Some name => quote name | None => "<unnamed>")
aspinall@15134
   389
  | None => "");
aspinall@15134
   390
aspinall@15134
   391
fun try_update_thy_only file =
aspinall@15134
   392
  ThyLoad.cond_add_path (Path.dir (Path.unpack file)) (fn () =>
aspinall@15134
   393
    let val name = thy_name file in
aspinall@15134
   394
      if is_some (ThyLoad.check_file (ThyLoad.thy_path name)) 
aspinall@15134
   395
      then update_thy_only name
aspinall@15134
   396
      else warning ("Unkown theory context of ML file." ^ which_context ())
aspinall@15134
   397
    end) ();
aspinall@15134
   398
aspinall@15134
   399
aspinall@15134
   400
(* get informed about files *)
aspinall@15134
   401
aspinall@15134
   402
val inform_file_retracted = 
aspinall@15134
   403
    ThyInfo.if_known_thy ThyInfo.remove_thy o thy_name;
aspinall@15134
   404
val inform_file_processed = 
aspinall@15134
   405
    ThyInfo.if_known_thy ThyInfo.touch_child_thys o thy_name;
aspinall@15134
   406
aspinall@15134
   407
fun proper_inform_file_processed file state =
aspinall@15134
   408
  let val name = thy_name file in
aspinall@15134
   409
    if Toplevel.is_toplevel state andalso ThyInfo.known_thy name then
aspinall@15134
   410
     (ThyInfo.touch_child_thys name;
aspinall@15134
   411
      transform_error ThyInfo.pretend_use_thy_only name handle ERROR_MESSAGE msg =>
aspinall@15134
   412
       (warning msg; warning ("Failed to register theory: " ^ quote name);
aspinall@15134
   413
        tell_file_retracted (Path.base (Path.unpack file))))
aspinall@15134
   414
    else raise Toplevel.UNDEF
aspinall@15134
   415
  end;
aspinall@15134
   416
aspinall@15134
   417
fun vacuous_inform_file_processed file state =
aspinall@15134
   418
 (warning ("No theory " ^ quote (thy_name file));
aspinall@15134
   419
  tell_file_retracted (Path.base (Path.unpack file)));
aspinall@15134
   420
aspinall@15134
   421
wenzelm@12778
   422
(* restart top-level loop (keeps most state information) *)
wenzelm@12778
   423
wenzelm@12778
   424
local
wenzelm@12778
   425
wenzelm@12778
   426
fun restart isar =
wenzelm@12778
   427
 (if isar then tell_clear_goals () else kill_goal ();
wenzelm@12778
   428
  tell_clear_response ();
wenzelm@12778
   429
  welcome ());
wenzelm@12778
   430
wenzelm@12778
   431
in
wenzelm@12778
   432
wenzelm@12778
   433
fun isa_restart () = restart false;
wenzelm@12778
   434
fun isar_restart () = (sync_thy_loader (); restart true; raise Toplevel.RESTART);
wenzelm@12778
   435
wenzelm@12778
   436
end;
wenzelm@12778
   437
wenzelm@12833
   438
fun full_proofs true = proofs := 2
wenzelm@12833
   439
  | full_proofs false = proofs := 1;
wenzelm@12833
   440
wenzelm@12833
   441
aspinall@15134
   442
(* theorem dependency output *)
aspinall@15134
   443
aspinall@15134
   444
local
aspinall@15134
   445
aspinall@15134
   446
val spaces_quote = space_implode " " o map quote;
aspinall@15134
   447
aspinall@15134
   448
fun thm_deps_message (thms, deps) = 
aspinall@15134
   449
    if pgip() then
aspinall@15134
   450
	issue_pgips 
aspinall@15134
   451
	    [XML.element
aspinall@15134
   452
		 "metainforesponse"  (* FIXME: get thy name from info here? *)
aspinall@15134
   453
		 [("infotype", "isabelle_theorem_dependencies")]
aspinall@15134
   454
		 [XML.element "value" [("name", "thms")] [XML.text thms],
aspinall@15134
   455
		  XML.element "value" [("name", "deps")] [XML.text deps]]]
aspinall@15134
   456
    else emacs_notify 
aspinall@15134
   457
	     ("Proof General, theorem dependencies of " 
aspinall@15134
   458
	      ^ thms ^ " are " ^ deps)
aspinall@15134
   459
aspinall@15134
   460
aspinall@15134
   461
fun tell_thm_deps ths =
aspinall@15134
   462
  conditional (thm_depsN mem_string ! print_mode) (fn () =>
aspinall@15134
   463
    let
aspinall@15134
   464
      val names = map Thm.name_of_thm ths \ "";
aspinall@15134
   465
      val deps = Symtab.keys (foldl (uncurry Proofterm.thms_of_proof)
aspinall@15134
   466
				    (Symtab.empty, map Thm.proof_of ths)) \ "";
aspinall@15134
   467
    in
aspinall@15134
   468
      if null names orelse null deps then ()
aspinall@15134
   469
      else thm_deps_message (spaces_quote names, spaces_quote deps)
aspinall@15134
   470
    end);
aspinall@15134
   471
aspinall@15134
   472
in
aspinall@15134
   473
aspinall@15134
   474
fun setup_present_hook () =
aspinall@15134
   475
  Present.add_hook (fn _ => fn res => tell_thm_deps (flat (map #2 res)));
aspinall@15134
   476
aspinall@15134
   477
end;
aspinall@15134
   478
aspinall@15134
   479
aspinall@15134
   480
(*** Preferences ***)
aspinall@15134
   481
aspinall@15134
   482
local
aspinall@15134
   483
val pgipnat        = XML.element "pgipint" [("min", "0")] [] 
aspinall@15134
   484
fun pgipnatmax max = XML.element "pgipint" [("min", "0"), 
aspinall@15134
   485
					    ("max", string_of_int max)] []
aspinall@15134
   486
val pgipbool       = XML.element "pgipbool" [] []
aspinall@15134
   487
aspinall@15134
   488
fun withdefault f = (f(), f)
aspinall@15134
   489
in
aspinall@15134
   490
aspinall@15134
   491
fun nat_option r = (pgipnat,
aspinall@15134
   492
  withdefault (fn () => string_of_int (!r)),
aspinall@15134
   493
  (fn s => (case Syntax.read_nat s of
aspinall@15134
   494
       None => error "nat_option: illegal value"
aspinall@15134
   495
     | Some i => r := i)));
aspinall@15134
   496
aspinall@15134
   497
fun bool_option r = (pgipbool,
aspinall@15134
   498
  withdefault (fn () => Bool.toString (!r)),
aspinall@15134
   499
  (fn "false" => r := false | "true" => r := true
aspinall@15134
   500
    | _ => error "bool_option: illegal value"));
aspinall@15134
   501
aspinall@15134
   502
val proof_option = (pgipbool,
aspinall@15134
   503
  withdefault (fn () => Bool.toString (!proofs >= 2)),
aspinall@15134
   504
  (fn "false" => proofs := 1 | "true" => proofs := 2
aspinall@15134
   505
    | _ => error "proof_option: illegal value"));
aspinall@15134
   506
aspinall@15134
   507
val thm_deps_option = (pgipbool,
aspinall@15134
   508
  withdefault (fn () => Bool.toString (Output.has_mode "thm_deps")),
aspinall@15134
   509
  (fn "false" => print_mode := ((!print_mode) \ "thm_deps")
aspinall@15134
   510
    | "true" => print_mode := ("thm_deps" ins (!print_mode))
aspinall@15134
   511
    | _ => error "thm_deps_option: illegal value"));
aspinall@15134
   512
aspinall@15134
   513
local 
aspinall@15134
   514
    val pg_print_depth_val = ref 10
aspinall@15134
   515
    fun pg_print_depth n = (print_depth n; pg_print_depth_val := n)
aspinall@15134
   516
in
aspinall@15134
   517
val print_depth_option = (pgipnat,
aspinall@15134
   518
  withdefault (fn () => string_of_int (!pg_print_depth_val)),
aspinall@15134
   519
  (fn s => (case Syntax.read_nat s of
aspinall@15134
   520
       None => error "print_depth_option: illegal value"
aspinall@15134
   521
     | Some i => pg_print_depth i)))
aspinall@15134
   522
end
aspinall@15134
   523
aspinall@15134
   524
val preferences = ref 
aspinall@15134
   525
  [("Display",
aspinall@15134
   526
    [("show-types", 
aspinall@15134
   527
      ("Include types in display of Isabelle terms", 
aspinall@15134
   528
       bool_option show_types)),
aspinall@15134
   529
     ("show-sorts", 
aspinall@15134
   530
      ("Include sorts in display of Isabelle terms", 
aspinall@15134
   531
       bool_option show_sorts)),
aspinall@15134
   532
     ("show-consts", 
aspinall@15134
   533
      ("Show types of consts in Isabelle goal display",
aspinall@15134
   534
       bool_option show_consts)),
aspinall@15134
   535
     ("long-names", 
aspinall@15134
   536
      ("Show fully qualified names in Isabelle terms", bool_option long_names)),
aspinall@15134
   537
     ("show-brackets", 
aspinall@15134
   538
      ("Show full bracketing in Isabelle terms",
aspinall@15134
   539
       bool_option show_brackets)),
aspinall@15134
   540
     ("show-main-goal", 
aspinall@15134
   541
      ("Show main goal in proof state display", bool_option Proof.show_main_goal)),
aspinall@15134
   542
     ("eta-contract", 
aspinall@15134
   543
      ("Print terms eta-contracted",
aspinall@15134
   544
       bool_option Syntax.eta_contract))]),
aspinall@15134
   545
   ("Advanced Display",
aspinall@15134
   546
    [("goals-limit", 
aspinall@15134
   547
      ("Setting for maximum number of goals printed",
aspinall@15134
   548
       nat_option goals_limit)),
aspinall@15134
   549
     ("prems-limit", 
aspinall@15134
   550
      ("Setting for maximum number of premises printed",
aspinall@15134
   551
       nat_option ProofContext.prems_limit)),
aspinall@15134
   552
     ("print-depth", 
aspinall@15134
   553
      ("Setting for the ML print depth",
aspinall@15134
   554
       print_depth_option))]),
aspinall@15134
   555
   ("Tracing",
aspinall@15134
   556
    [("trace-simplifier", 
aspinall@15134
   557
      ("Trace simplification rules.",
aspinall@15134
   558
       bool_option trace_simp)),
aspinall@15134
   559
     ("trace-rules", ("Trace application of the standard rules",
aspinall@15134
   560
		      bool_option trace_rules)),
aspinall@15134
   561
     ("trace-unification", 
aspinall@15134
   562
      ("Output error diagnostics during unification",
aspinall@15134
   563
       bool_option Pattern.trace_unify_fail)),
aspinall@15134
   564
     ("global-timing", 
aspinall@15134
   565
      ("Whether to enable timing in Isabelle.",
aspinall@15134
   566
       bool_option Output.timing))]),
aspinall@15134
   567
   ("Proof", 
aspinall@15134
   568
    [("quick-and-dirty", 
aspinall@15134
   569
      ("Take a few (interactive-only) short cuts",
aspinall@15134
   570
       bool_option quick_and_dirty)),
aspinall@15134
   571
     ("full-proofs", 
aspinall@15134
   572
      ("Record full proof objects internally",
aspinall@15134
   573
       proof_option)),
aspinall@15134
   574
     ("theorem-dependencies", 
aspinall@15134
   575
       ("Track theorem dependencies within Proof General",
aspinall@15134
   576
	thm_deps_option))])
aspinall@15134
   577
   ];
aspinall@15134
   578
end
aspinall@15134
   579
aspinall@15134
   580
(* Configuration: GUI config, proverinfo messages *)
aspinall@15134
   581
aspinall@15134
   582
local
aspinall@15134
   583
    val config_file = "~~/lib/ProofGeneral/pgip_isar.xml"
aspinall@15134
   584
    val name_attr = pair "name"
aspinall@15134
   585
    val version_attr = pair "version"
aspinall@15134
   586
    val isabelle_www = "http://isabelle.in.tum.de/"
aspinall@15134
   587
in
aspinall@15134
   588
fun send_pgip_config () =
aspinall@15134
   589
    let 
aspinall@15134
   590
	val path = Path.unpack config_file
aspinall@15134
   591
	val exists = File.exists path
aspinall@15134
   592
	val proverinfo = 
aspinall@15134
   593
	    XML.element "proverinfo"
aspinall@15134
   594
              [("name",Session.name()), ("version", version),
aspinall@15134
   595
	       ("url", isabelle_www)]
aspinall@15134
   596
	    [XML.element "welcomemsg" [] [XML.text (Session.welcome())],
aspinall@15134
   597
	     XML.element "helpdoc" 
aspinall@15134
   598
         (* NB: would be nice to generate/display docs from isatool
aspinall@15134
   599
          doc, but that program may not be running on same machine;
aspinall@15134
   600
          front end should be responsible for launching viewer, etc. *)
aspinall@15134
   601
		      [("name", "Isabelle/HOL Tutorial"),
aspinall@15134
   602
		       ("descr", "A Gentle Introduction to Isabelle/HOL"), 
aspinall@15134
   603
		       ("url",  "http://isabelle.in.tum.de/dist/Isabelle2003/doc/tutorial.pdf")]
aspinall@15134
   604
	      []]
aspinall@15134
   605
    in
aspinall@15134
   606
	if exists then
aspinall@15134
   607
	    (issue_pgips [proverinfo]; issue_pgips [File.read path])
aspinall@15134
   608
	else panic ("PGIP configuration file " ^ config_file ^ " not found")
aspinall@15134
   609
    end;
aspinall@15134
   610
end
aspinall@15134
   611
aspinall@15134
   612
aspinall@15134
   613
(* PGIP identifier tables (prover objects). [incomplete] *)
aspinall@15134
   614
aspinall@15134
   615
local
aspinall@15134
   616
    val objtype_thy  = "theory"
aspinall@15134
   617
    val objtype_thm  = "theorem"
aspinall@15134
   618
    val objtype_term = "term"
aspinall@15134
   619
    val objtype_type = "type"
aspinall@15134
   620
		       
aspinall@15134
   621
    fun xml_idtable ty ctx ids = 
aspinall@15134
   622
	let
aspinall@15134
   623
            fun ctx_attr (Some c)= [("context", c)]
aspinall@15134
   624
              | ctx_attr None    = []
aspinall@15134
   625
	    fun xmlid x = XML.element "identifier" [] [XML.text x];
aspinall@15134
   626
	in 
aspinall@15134
   627
	    XML.element "idtable" (("objtype", ty)::ctx_attr ctx)
aspinall@15134
   628
	                          (map xmlid ids)
aspinall@15134
   629
	end
aspinall@15134
   630
in
aspinall@15134
   631
aspinall@15134
   632
fun setids t = issue_pgip "setids" [] t
aspinall@15134
   633
fun addids t = issue_pgip "addids" [] t
aspinall@15134
   634
fun delids t = issue_pgip "delids" [] t
aspinall@15134
   635
aspinall@15134
   636
fun delallids ty = setids (xml_idtable ty None [])
aspinall@15134
   637
aspinall@15134
   638
fun send_thy_idtable ctx thys = setids (xml_idtable objtype_thy ctx thys)
aspinall@15134
   639
fun clear_thy_idtable () = delallids objtype_thy
aspinall@15134
   640
aspinall@15134
   641
fun send_thm_idtable ctx thy = 
aspinall@15134
   642
    addids (xml_idtable objtype_thm ctx (map fst (PureThy.thms_of thy)));
aspinall@15134
   643
aspinall@15134
   644
fun clear_thm_idtable () = delallids objtype_thm
aspinall@15134
   645
aspinall@15134
   646
(* fun send_type_idtable thy = TODO, it's a bit low-level messy
aspinall@15134
   647
   & maybe not so useful anyway *)
aspinall@15134
   648
	
aspinall@15134
   649
end
aspinall@15134
   650
aspinall@15134
   651
(* Response to interface queries about known objects *)
aspinall@15134
   652
aspinall@15134
   653
local
aspinall@15134
   654
 val topthy = Toplevel.theory_of o Toplevel.get_state
aspinall@15134
   655
 val pthm = print_thm oo get_thm
aspinall@15134
   656
aspinall@15134
   657
 fun idvalue tp nm = ("idvalue",[("objtype",tp),("name",nm)])
aspinall@15134
   658
in
aspinall@15134
   659
fun askids (None, Some "theory")  = send_thy_idtable None (ThyInfo.names())
aspinall@15134
   660
  | askids (None, None) =  send_thy_idtable None (ThyInfo.names())
aspinall@15134
   661
                           (* only theories known in top context *)
aspinall@15134
   662
  | askids (Some thy, Some "theory") = send_thy_idtable (Some thy) (ThyInfo.get_preds thy)
aspinall@15134
   663
  | askids (Some thy, Some "theorem") = send_thm_idtable (Some thy) (ThyInfo.get_theory thy)
aspinall@15134
   664
  | askids (Some thy, None) = (send_thy_idtable (Some thy) (ThyInfo.get_preds thy);
aspinall@15134
   665
                               send_thm_idtable (Some thy) (ThyInfo.get_theory thy)) 
aspinall@15134
   666
(*  | askids (Some thy, "type") = send_type_idtable (Some thy) (ThyInfo.get_theory thy) *)
aspinall@15134
   667
  | askids (_, Nothing) = error "No objects of any type are available here."
aspinall@15134
   668
  | askids (_, Some ot) = error ("No objects of type "^(quote ot)^" are available here.")
aspinall@15134
   669
aspinall@15134
   670
fun showid (_,        "theory", n) = 
aspinall@15134
   671
    with_displaywrap (idvalue "theory" n) (fn ()=>(print_theory (ThyInfo.get_theory n)))
aspinall@15134
   672
  | showid (Some thy, "theorem", t) = 
aspinall@15134
   673
    with_displaywrap (idvalue "theorem" t) (fn ()=>(pthm (ThyInfo.get_theory thy) t))
aspinall@15134
   674
  | showid (None,     "theorem", t) = 
aspinall@15134
   675
    with_displaywrap (idvalue "theorem" t) (fn ()=>pthm (topthy()) t)
aspinall@15134
   676
  | showid (_, ot, _) = error ("Cannot show objects of type "^ot)
aspinall@15134
   677
aspinall@15134
   678
(* Return script command to set an identifier to some value *)
aspinall@15134
   679
(* TODO: support object preference setting here *)
aspinall@15134
   680
fun bindid (name, "thm", [XML.Elem ("objval",_,[XML.Text objval])]) = 
aspinall@15134
   681
    ("lemmas " ^ name ^ " = " ^ objval)
aspinall@15134
   682
  | bindid (name, ot, _) = error ("Cannot bind objects of type " ^ ot)
aspinall@15134
   683
aspinall@15134
   684
end
aspinall@15134
   685
	 
aspinall@15134
   686
(** Parsing proof scripts without execution **)
aspinall@15134
   687
aspinall@15134
   688
local
aspinall@15134
   689
    (* This is a temporary hack until we have decent parsing of proof scripts *)
aspinall@15134
   690
    fun xmle elt = XML.element elt [] []
aspinall@15134
   691
    fun xmlc elt str = XML.element elt [] [XML.text str]
aspinall@15134
   692
aspinall@15134
   693
    fun make_opengoal args =
aspinall@15134
   694
	(* For now, strictly only args like <lemma foo: "P->Q"> *)
aspinall@15134
   695
	let
aspinall@15134
   696
	    val tstart = find_index_eq "\"" (explode args)
aspinall@15134
   697
	    val tend = find_index_eq "\"" (drop (tstart, (explode args)))
aspinall@15134
   698
	    val nend = find_index_eq ":" (explode args)
aspinall@15134
   699
	    val uptonend = (rev (take (nend-1,explode args)))
aspinall@15134
   700
	    val nstart = (length uptonend) - 
aspinall@15134
   701
			 (find_index (not o Symbol.is_letter) uptonend)
aspinall@15134
   702
	in 
aspinall@15134
   703
	    (XML.element 
aspinall@15134
   704
		"opengoal" 
aspinall@15134
   705
		[("thmname", String.substring(args,nstart,nend-nstart))]
aspinall@15134
   706
		[XML.text (String.substring(args, tstart+1, tend))])
aspinall@15134
   707
	end
aspinall@15134
   708
aspinall@15134
   709
    fun make_theory args =
aspinall@15134
   710
	(* For now, strictly only args like <theory Foo=Main:> *)
aspinall@15134
   711
	let
aspinall@15134
   712
	    val argstart = find_index_eq "=" (explode args)
aspinall@15134
   713
	    val argend = find_index_eq ":" (explode args)
aspinall@15134
   714
	    val (name1,arg1) = splitAt(argstart, explode args)
aspinall@15134
   715
	    val namecs = dropwhile (fn c => c mem [" ","\t","\n"]) (rev name1)
aspinall@15134
   716
	    val nameend = find_index (fn c=> not (Symbol.is_quasi_letter c)) namecs
aspinall@15134
   717
	    val (namecs',_) = splitAt(nameend, namecs)
aspinall@15134
   718
	    val name = implode (rev namecs')
aspinall@15134
   719
	    val (arg2, _) = splitAt(argend-argstart-1, tl arg1)
aspinall@15134
   720
            val arg = implode arg2
aspinall@15134
   721
	in 
aspinall@15134
   722
	    XML.element "opentheory" [("thyname", name)] [XML.text arg]
aspinall@15134
   723
	end
aspinall@15134
   724
in
aspinall@15134
   725
fun xmls_of_transition (name,toks,tr) = 
aspinall@15134
   726
   let 
aspinall@15134
   727
       val str = name ^ " " ^ (space_implode " " (map OuterLex.unparse toks))
aspinall@15134
   728
   in
aspinall@15134
   729
    case name of (* NB: see isar_syn.ML for names of standard commands *)
aspinall@15134
   730
         "done"       => [xmle "closegoal"]  
aspinall@15134
   731
       | "sorry"      => [xmle "giveupgoal"]
aspinall@15134
   732
       | "oops"       => [xmle "postponegoal"]
aspinall@15134
   733
       | "by"         => [xmlc "proofstep" ("apply " ^ str),
aspinall@15134
   734
			  xmle "closegoal"] (* FIXME: tactic proofs only just now *)
aspinall@15134
   735
       (* theories *)
aspinall@15134
   736
       | "theory"     => [make_theory str]
aspinall@15134
   737
       (* goals *)
aspinall@15134
   738
       | "lemma"      => [make_opengoal str]
aspinall@15134
   739
       | "theorem"    => [make_opengoal str]
aspinall@15134
   740
       | "corollary"  => [make_opengoal str]
aspinall@15134
   741
       (* literate text *)
aspinall@15134
   742
       | "text"       => [xmlc "litcomment" str]
aspinall@15134
   743
       | "sect"       => [xmlc "litcomment" ("ion " ^ str)]
aspinall@15134
   744
       | "subsect"    => [xmlc "litcomment" ("ion " ^ str)]
aspinall@15134
   745
       | "subsubsect" => [xmlc "litcomment" ("ion " ^ str)]
aspinall@15134
   746
       | "txt"	      => [xmlc "litcomment" str]
aspinall@15134
   747
       | _ => [xmlc "proofstep" str]  (* default for anything else *)
aspinall@15134
   748
   end
aspinall@15134
   749
aspinall@15134
   750
(* FIXME: need to handle parse errors gracefully below, perhaps returning partial parse *)
aspinall@15134
   751
(* NB: comments are ignored by below; not good if we use this to reconstruct script *)
aspinall@15134
   752
aspinall@15134
   753
fun xmls_of_str str =
aspinall@15134
   754
   let fun parse_loop (nm_lex_trs,xmls) = 
aspinall@15134
   755
	   (case nm_lex_trs of
aspinall@15134
   756
	      [] => xmls  
aspinall@15134
   757
	    | (nm,toks,tr)::rest  => 
aspinall@15134
   758
	      let 
aspinall@15134
   759
		val xmls_tr = xmls_of_transition (nm,toks,tr)
aspinall@15134
   760
	      in  
aspinall@15134
   761
	         parse_loop (rest, xmls @ xmls_tr)
aspinall@15134
   762
	      end)
aspinall@15134
   763
    in
aspinall@15134
   764
	parse_loop (OuterSyntax.read str, [])
aspinall@15134
   765
    end
aspinall@15134
   766
aspinall@15134
   767
aspinall@15134
   768
fun parsescript str = 
aspinall@15134
   769
    issue_pgips [XML.element "parseresult" [] (xmls_of_str str)]
aspinall@15134
   770
aspinall@15134
   771
end
aspinall@15134
   772
aspinall@15134
   773
aspinall@15134
   774
aspinall@15134
   775
(**** PGIP:  Isabelle -> Interface ****)
aspinall@15134
   776
aspinall@15134
   777
val isabelle_pgml_version_supported = "1.0"; 
aspinall@15134
   778
val isabelle_pgip_version_supported = "1.0"
aspinall@15134
   779
aspinall@15134
   780
fun usespgip () = 
aspinall@15134
   781
    issue_pgipe "usespgip" [("version", isabelle_pgip_version_supported)];
aspinall@15134
   782
aspinall@15134
   783
fun usespgml () = 
aspinall@15134
   784
    issue_pgipe "usespgml" [("version", isabelle_pgml_version_supported)];
aspinall@15134
   785
aspinall@15134
   786
fun hasprefs () = 
aspinall@15134
   787
    seq (fn (prefcat, prefs) =>
aspinall@15134
   788
	    issue_pgips [XML.element "hasprefs" [("prefcategory",prefcat)]
aspinall@15134
   789
		 (map (fn (name, (descr, (ty, (default,_),_))) => 
aspinall@15134
   790
		       XML.element "haspref" [("name", name), 
aspinall@15134
   791
					      ("descr", descr), 
aspinall@15134
   792
					      ("default", default)]
aspinall@15134
   793
		       [ty]) prefs)]) (!preferences);
aspinall@15134
   794
aspinall@15134
   795
fun allprefs () = foldl (op @) ([], map snd (!preferences))
aspinall@15134
   796
	
aspinall@15134
   797
fun setpref name value = 
aspinall@15134
   798
    (case assoc (allprefs(), name) of
aspinall@15134
   799
	 None => warning ("Unknown pref: " ^ quote name)
aspinall@15134
   800
       | Some (_, (_, _, set)) => set value);
aspinall@15134
   801
aspinall@15134
   802
fun getpref name = 
aspinall@15134
   803
    (case assoc (allprefs(), name) of
aspinall@15134
   804
	 None => warning ("Unknown pref: " ^ quote name)
aspinall@15134
   805
       | Some (_, (_, (_,get), _)) => 
aspinall@15134
   806
	   issue_pgip "prefval" [("name", name)] (get ()));
aspinall@15134
   807
aspinall@15134
   808
aspinall@15134
   809
aspinall@15134
   810
aspinall@15134
   811
aspinall@15134
   812
(**** PGIP:  Interface -> Isabelle/Isar ****)
aspinall@15134
   813
aspinall@15134
   814
exception PGIP of string;
aspinall@15134
   815
exception PGIP_QUIT;
aspinall@15134
   816
aspinall@15134
   817
(* Sending commands to Isar *)
aspinall@15134
   818
aspinall@15134
   819
(* FIXME Makarius:
aspinall@15134
   820
   'isarcmd': consider using 'Toplevel.>>>' instead of
aspinall@15134
   821
   'Toplevel.loop'; unsure about the exact error behaviour required here;
aspinall@15134
   822
*)
aspinall@15134
   823
val isarcmd = Toplevel.loop o
aspinall@15134
   824
		(OuterSyntax.isar_readstring 
aspinall@15134
   825
		    (Position.name "PGIP message")) (* FIXME: could do better *)
aspinall@15134
   826
aspinall@15134
   827
fun isarscript s = isarcmd s   (* send a script command *)
aspinall@15134
   828
   (* was: (isarcmd s;  issue_pgip "scriptinsert" [] (XML.text s)) *)
aspinall@15134
   829
aspinall@15134
   830
aspinall@15134
   831
(* load an arbitrary (.thy or .ML) file *)
aspinall@15134
   832
aspinall@15134
   833
fun use_thy_or_ml_file file = 
aspinall@15134
   834
    let
aspinall@15134
   835
	val (path,extn) = Path.split_ext (Path.unpack file)
aspinall@15134
   836
    in
aspinall@15134
   837
	case extn of
aspinall@15134
   838
	    "" => isarcmd ("use_thy " ^ (quote (Path.pack path)))
aspinall@15134
   839
	  | "thy" => isarcmd ("use_thy " ^ (quote (Path.pack path)))
aspinall@15134
   840
	  | "ML" => isarcmd ("use " ^ quote file)
aspinall@15134
   841
	  (* instead of error we could guess theory? *)
aspinall@15134
   842
	  | other => error ("Don't know how to read a file with extension " ^ other)
aspinall@15134
   843
    end  
aspinall@15134
   844
aspinall@15134
   845
aspinall@15134
   846
local
aspinall@15134
   847
  (* Proof control commands *)
aspinall@15134
   848
aspinall@15134
   849
  fun xmlattro attrs attr = assoc(attrs,attr)
aspinall@15134
   850
aspinall@15134
   851
  fun xmlattr attrs attr = 
aspinall@15134
   852
      (case xmlattro attrs attr of 
aspinall@15134
   853
	   Some value => value 
aspinall@15134
   854
	 | None => raise PGIP ("Missing attribute: " ^ attr))
aspinall@15134
   855
aspinall@15134
   856
  fun xmltext [XML.Text text] = text
aspinall@15134
   857
    | xmltext ((XML.Text text)::ts) = text ^ " " ^ (xmltext ts)  (* FIXME: space shouldn't be needed *)
aspinall@15134
   858
    | xmltext _ = raise PGIP "Expected text (PCDATA/CDATA)"
aspinall@15134
   859
			
aspinall@15134
   860
  val thyname_attr = "thyname"
aspinall@15134
   861
  val objtype_attr = "objtype"
aspinall@15134
   862
  val name_attr = "name"
aspinall@15134
   863
  val dirname_attr = "dir"
aspinall@15134
   864
  fun comment x = "(* " ^ x ^ " *)"
aspinall@15134
   865
aspinall@15134
   866
(* return script portion corresponding to a PGIP command.
aspinall@15134
   867
   We only unparse proper proof commands. 
aspinall@15134
   868
   (we might unparse gui opns too, if they didn't have opcmd settings?)
aspinall@15134
   869
*)
aspinall@15134
   870
  fun unparse (elem,attrs,xmls) = 
aspinall@15134
   871
      (case elem of 
aspinall@15134
   872
         "opengoal" => "lemma " ^ (xmlattr attrs "thmname") ^ ": " ^
aspinall@15134
   873
					  (quote (xmltext xmls))
aspinall@15134
   874
	  (* FIXME: should maybe remove    ^^^^^^^^^^ 
aspinall@15134
   875
	     to provide for Isar's parenthetical phrases (is ...) *)
aspinall@15134
   876
       | "proofstep" => xmltext xmls
aspinall@15134
   877
       | "closegoal" => "done"   (* FIXME: or qed? Maybe nothing? *)
aspinall@15134
   878
aspinall@15134
   879
       | "opentheory" => ("theory " ^ (xmlattr attrs thyname_attr) ^ 
aspinall@15134
   880
					" = " ^ (xmltext xmls) ^ ":")
aspinall@15134
   881
       | "closetheory" => "end"
aspinall@15134
   882
       | "postponegoal" => "sorry"
aspinall@15134
   883
       | "giveupgoal" => "oops"
aspinall@15134
   884
aspinall@15134
   885
       | "bindid" => (bindid (xmlattr attrs objtype_attr, 
aspinall@15134
   886
				 xmlattr attrs name_attr, 
aspinall@15134
   887
				 xmls))
aspinall@15134
   888
       | "comment" => comment (xmltext xmls)
aspinall@15134
   889
       | "litcomment" => xmltext xmls
aspinall@15134
   890
       | _ => error ("unparse called with improper proof command: " ^ elem))
aspinall@15134
   891
aspinall@15134
   892
  fun unparsecmds xmls = 
aspinall@15134
   893
      let
aspinall@15134
   894
	  fun upc (XML.Elem elt) = (unparse elt) 
aspinall@15134
   895
	    | upc (XML.Text t) = (warning ("unprasecmds: ignoring spurious text: " ^ t); "")
aspinall@15134
   896
      in 
aspinall@15134
   897
	  issue_pgip "unparseresult" [] 
aspinall@15134
   898
		     (XML.text (cat_lines (map upc xmls))) (* FIXME: use cdata? *)
aspinall@15134
   899
      end
aspinall@15134
   900
aspinall@15134
   901
  (* parse URLs like "file://host/name.thy" *)
aspinall@15134
   902
  (* FIXME: instead of this, extend code in General/url.ML & use that. *)
aspinall@15134
   903
  fun decode_url url = 
aspinall@15134
   904
      (let 
aspinall@15134
   905
	  val sep = find_index_eq ":" (explode url)
aspinall@15134
   906
 	  val proto = String.substring(url,0,sep)
aspinall@15134
   907
	  val hostsep = find_index_eq "/" (drop (sep+3,explode url))
aspinall@15134
   908
	  val host = String.substring(url,sep+3,hostsep-sep+4)
aspinall@15134
   909
	  val doc = if (size url >= sep+hostsep+3) then
aspinall@15134
   910
			String.substring(url,sep+hostsep+4,size url-hostsep-sep-4) 
aspinall@15134
   911
		    else ""
aspinall@15134
   912
      in 
aspinall@15134
   913
	  (proto,host,doc)
aspinall@15134
   914
      end) handle Subscript => error ("Badly formed URL " ^ url)
aspinall@15134
   915
 
aspinall@15134
   916
  fun localfile_of_url url =
aspinall@15134
   917
      let
aspinall@15134
   918
	  val (proto,host,name) = decode_url url
aspinall@15134
   919
      in
aspinall@15134
   920
	  if (proto = "file" andalso 
aspinall@15134
   921
	      (host = "" orelse 
aspinall@15134
   922
	       host = "localhost" orelse 
aspinall@15134
   923
	       host = (getenv "HOSTNAME")))
aspinall@15134
   924
	     then name
aspinall@15134
   925
	  else error ("Cannot access non-local URL " ^ url)
aspinall@15134
   926
      end
aspinall@15134
   927
aspinall@15134
   928
  fun fileurl_of attrs = localfile_of_url (xmlattr attrs "url")
aspinall@15134
   929
aspinall@15134
   930
  val topthy = Toplevel.theory_of o Toplevel.get_state
aspinall@15134
   931
  val topthy_name = PureThy.get_name o topthy
aspinall@15134
   932
aspinall@15134
   933
  val currently_open_file = ref (None : string option)
aspinall@15134
   934
in
aspinall@15134
   935
aspinall@15134
   936
fun process_pgip_element pgipxml =
aspinall@15134
   937
    (case pgipxml of 
aspinall@15134
   938
	 (XML.Text t) => warning ("Ignored text in PGIP packet: \n" ^ t)
aspinall@15134
   939
       | (XML.Elem (xml as (elem, attrs, xmls))) => (case elem of
aspinall@15134
   940
(* protocol config *)
aspinall@15134
   941
  "askpgip"  	   => (usespgip (); send_pgip_config ())
aspinall@15134
   942
| "askpgml"  	   => usespgml ()
aspinall@15134
   943
(* proverconfig *)
aspinall@15134
   944
| "askprefs" 	   => hasprefs ()
aspinall@15134
   945
| "getpref"  	   => getpref (xmlattr attrs name_attr)
aspinall@15134
   946
| "setpref"  	   => setpref (xmlattr attrs name_attr) (xmltext xmls)
aspinall@15134
   947
(* provercontrol *)
aspinall@15134
   948
| "proverinit" 	   => isar_restart ()
aspinall@15134
   949
| "proverexit" 	   => isarcmd "quit"
aspinall@15134
   950
| "startquiet" 	   => isarcmd "disable_pr"
aspinall@15134
   951
| "stopquiet"  	   => isarcmd "enable_pr"
aspinall@15134
   952
| "pgmlsymbolson"  => (print_mode := (["xsymbols", "symbols"] @ ! print_mode))
aspinall@15134
   953
| "pgmlsymbolsoff" => (print_mode := (Library.gen_rems 
aspinall@15134
   954
					  (op =) (! print_mode, ["xsymbols", "symbols"])))
aspinall@15134
   955
(* provercmd: proper commands which belong in script *)
aspinall@15134
   956
| "proofstep"      => isarscript (unparse xml)
aspinall@15134
   957
| "opengoal"       => isarscript (unparse xml)
aspinall@15134
   958
| "closegoal"      => isarscript (unparse xml)
aspinall@15134
   959
| "postponegoal"   => isarscript (unparse xml)
aspinall@15134
   960
| "giveupgoal"     => isarscript (unparse xml)
aspinall@15134
   961
| "comment"	   => isarscript (unparse xml)
aspinall@15134
   962
| "litcomment"	   => isarscript (unparse xml)
aspinall@15134
   963
(* provercmd: improper commands which *do not* belong in script *)
aspinall@15134
   964
| "undostep"       => isarcmd "ProofGeneral.undo"
aspinall@15134
   965
| "abortgoal"      => isarcmd "ProofGeneral.kill_proof"  
aspinall@15134
   966
| "forget"         => error ("Not implemented") 
aspinall@15134
   967
| "restoregoal"    => error ("Not implemented")  (* could just treat as forget? *)
aspinall@15134
   968
(* proofctxt: improper commands *)
aspinall@15134
   969
| "askids"         => askids (xmlattro attrs thyname_attr, 
aspinall@15134
   970
		              xmlattro attrs objtype_attr)
aspinall@15134
   971
| "showid"	   => showid (xmlattro attrs thyname_attr, 
aspinall@15134
   972
		              xmlattr attrs objtype_attr,
aspinall@15134
   973
		     	      xmlattr attrs name_attr)
aspinall@15134
   974
| "parsescript"    => parsescript (xmltext xmls)
aspinall@15134
   975
| "unparsecmds"    => unparsecmds xmls
aspinall@15134
   976
| "showproofstate" => isarcmd "pr"
aspinall@15134
   977
| "showctxt"       => isarcmd "print_theory" (* more useful than print_context *)
aspinall@15134
   978
| "searchtheorems" => isarcmd ("thms_containing " ^ (xmltext xmls))
aspinall@15134
   979
| "setlinewidth"   => isarcmd ("pretty_setmargin " ^ (xmltext xmls))
aspinall@15134
   980
(* proofctxt: proper commands *)
aspinall@15134
   981
| "bindid"         => isarscript (unparse xml)
aspinall@15134
   982
(* filecmd: proper commands *)
aspinall@15134
   983
| "opentheory"     => isarscript (unparse xml)
aspinall@15134
   984
| "closetheory"    => (isarscript (unparse xml);
aspinall@15134
   985
		       writeln ("Theory "^(topthy_name())^" completed."))
aspinall@15134
   986
(* filecmd: improper commands *)
aspinall@15134
   987
| "aborttheory"    => isarcmd ("init_toplevel")
aspinall@15134
   988
| "retracttheory"  => isarcmd ("kill_thy " ^
aspinall@15134
   989
			       (quote (xmlattr attrs thyname_attr)))
aspinall@15134
   990
| "loadfile"       => use_thy_or_ml_file    (fileurl_of attrs)
aspinall@15134
   991
| "openfile"       => (inform_file_retracted (fileurl_of attrs);
aspinall@15134
   992
		       currently_open_file := Some (fileurl_of attrs))
aspinall@15134
   993
| "closefile"      => (case !currently_open_file of 
aspinall@15134
   994
			   Some f => (inform_file_processed f;
aspinall@15134
   995
				      currently_open_file := None)
aspinall@15134
   996
			 | None => raise PGIP ("closefile when no file is open!"))
aspinall@15134
   997
| "abortfile"      => (currently_open_file := None) (* might give error for no file open *)
aspinall@15134
   998
| "changecwd"      => ThyLoad.add_path (xmlattr attrs dirname_attr)
aspinall@15134
   999
(* unofficial command for debugging *)
aspinall@15134
  1000
| "quitpgip" => raise PGIP_QUIT  
aspinall@15134
  1001
| _ => raise PGIP ("Unrecognized PGIP element: " ^ elem)))
aspinall@15134
  1002
aspinall@15134
  1003
fun process_pgip_tree s = 
aspinall@15134
  1004
    (pgip_refseq := None; 
aspinall@15134
  1005
     pgip_refid := None;
aspinall@15134
  1006
     (case s of
aspinall@15134
  1007
	  XML.Elem ("pgip", attrs, pgips) => 
aspinall@15134
  1008
	  (let 
aspinall@15134
  1009
	       val class = xmlattr attrs "class"
aspinall@15134
  1010
	       val _ = (pgip_refseq := xmlattro attrs "seq";
aspinall@15134
  1011
			pgip_refid :=  xmlattro attrs "id")
aspinall@15134
  1012
	   in  
aspinall@15134
  1013
	       if (class = "pa") then
aspinall@15134
  1014
		   seq process_pgip_element pgips
aspinall@15134
  1015
	       else 
aspinall@15134
  1016
		   raise PGIP "PGIP packet for me should have class=\"pa\""
aspinall@15134
  1017
	   end)
aspinall@15134
  1018
	| _ => raise PGIP "Invalid PGIP packet received") 
aspinall@15134
  1019
     handle (PGIP msg) => 
aspinall@15134
  1020
	    (error (msg ^ "\nPGIP error occured in XML text below:\n" ^ 
aspinall@15134
  1021
		    (XML.string_of_tree s))))
aspinall@15134
  1022
aspinall@15134
  1023
(* for export to Emacs *)
aspinall@15134
  1024
(* val process_pgip = process_pgip_tree o XML.tree_of_string; *)
aspinall@15134
  1025
(* FIXME: for temporary compatibility with PG 3.4, we engage special characters
aspinall@15134
  1026
   during output *)
aspinall@15134
  1027
fun process_pgip s = 
aspinall@15134
  1028
    (pgip_emacs_compatibility_flag := true;
aspinall@15134
  1029
     process_pgip_tree (XML.tree_of_string s);
aspinall@15134
  1030
     pgip_emacs_compatibility_flag := false)
aspinall@15134
  1031
end
aspinall@15134
  1032
aspinall@15134
  1033
aspinall@15134
  1034
aspinall@15134
  1035
aspinall@15134
  1036
(* PGIP loop: process PGIP input only *)
aspinall@15134
  1037
aspinall@15134
  1038
local  
aspinall@15134
  1039
(* NB: simple tty for now; later might read from other sources, open sockets, etc. *)
aspinall@15134
  1040
(* FIXME da: doesn't setting the stopper at a single element mean we have to
aspinall@15134
  1041
  parse the whole tree on one go anyway? *)
aspinall@15134
  1042
val tty_src = Source.set_prompt ""
aspinall@15134
  1043
	      (Source.source Symbol.stopper (XML.parse_elem >> single)
aspinall@15134
  1044
					None Source.tty);
aspinall@15134
  1045
aspinall@15134
  1046
(* FIXME: Makarius:
aspinall@15134
  1047
 'read_pgip()': some content may be left in the internal buffer after
aspinall@15134
  1048
 Source.get_single, which will got lost between calls; try to avoid
aspinall@15134
  1049
 building the tty source over and over again;
aspinall@15134
  1050
*)
aspinall@15134
  1051
aspinall@15134
  1052
fun read_pgip () =  Source.get_single tty_src
aspinall@15134
  1053
aspinall@15134
  1054
fun loop () =
aspinall@15134
  1055
    let 
aspinall@15134
  1056
	val _ = issue_pgipe "ready" []
aspinall@15134
  1057
    in
aspinall@15134
  1058
	case (read_pgip()) of  
aspinall@15134
  1059
	     None  => ()
aspinall@15134
  1060
	   | Some (pgip,_) =>  (process_pgip_tree pgip; loop()) handle e => handler e
aspinall@15134
  1061
    end handle e => handler e
aspinall@15134
  1062
aspinall@15134
  1063
and handler e = 
aspinall@15134
  1064
    case e of
aspinall@15134
  1065
        PGIP_QUIT => ()
aspinall@15134
  1066
      | ERROR => loop() (* message already given *)
aspinall@15134
  1067
      | Interrupt => (error "Interrupt during PGIP processing"; loop())
aspinall@15134
  1068
      | Toplevel.UNDEF => (error "No working context defined"; loop()) (* usually *)
aspinall@15134
  1069
      | e => (error (Toplevel.exn_message e); loop())
aspinall@15134
  1070
      (* Also seen: Scan.FAIL (not exported from Scan -- needs catching in xml.ML) *)
aspinall@15134
  1071
in
aspinall@15134
  1072
   val pgip_toplevel =  loop
aspinall@15134
  1073
end
aspinall@15134
  1074
aspinall@15134
  1075
aspinall@15134
  1076
(* additional outer syntax for Isar *)
wenzelm@12778
  1077
wenzelm@12778
  1078
local structure P = OuterParse and K = OuterSyntax.Keyword in
wenzelm@12778
  1079
aspinall@15134
  1080
val undoP = (* undo without output *)
wenzelm@12778
  1081
  OuterSyntax.improper_command "ProofGeneral.undo" "(internal)" K.control
wenzelm@12778
  1082
    (Scan.succeed (Toplevel.no_timing o IsarCmd.undo));
wenzelm@12778
  1083
wenzelm@12778
  1084
val context_thy_onlyP =
wenzelm@12778
  1085
  OuterSyntax.improper_command "ProofGeneral.context_thy_only" "(internal)" K.control
wenzelm@12778
  1086
    (P.name >> (Toplevel.no_timing oo IsarThy.init_context update_thy_only));
wenzelm@12778
  1087
wenzelm@12778
  1088
val try_context_thy_onlyP =
wenzelm@12778
  1089
  OuterSyntax.improper_command "ProofGeneral.try_context_thy_only" "(internal)" K.control
wenzelm@12778
  1090
    (P.name >> (Toplevel.no_timing oo
wenzelm@12778
  1091
      (Toplevel.imperative (K ()) oo IsarThy.init_context try_update_thy_only)));
wenzelm@12778
  1092
wenzelm@12778
  1093
val restartP =
wenzelm@12778
  1094
  OuterSyntax.improper_command "ProofGeneral.restart" "(internal)" K.control
wenzelm@12778
  1095
    (P.opt_unit >> (Toplevel.no_timing oo K (Toplevel.imperative isar_restart)));
wenzelm@12778
  1096
wenzelm@12778
  1097
val kill_proofP =
wenzelm@12778
  1098
  OuterSyntax.improper_command "ProofGeneral.kill_proof" "(internal)" K.control
wenzelm@12778
  1099
    (Scan.succeed (Toplevel.no_timing o IsarCmd.kill_proof_notify tell_clear_goals));
wenzelm@12778
  1100
wenzelm@12778
  1101
val inform_file_processedP =
wenzelm@12778
  1102
  OuterSyntax.improper_command "ProofGeneral.inform_file_processed" "(internal)" K.control
wenzelm@14902
  1103
    (P.name >> (fn file => Toplevel.no_timing o
wenzelm@14902
  1104
      Toplevel.keep (vacuous_inform_file_processed file) o
wenzelm@14902
  1105
      Toplevel.kill o
wenzelm@14902
  1106
      Toplevel.keep (proper_inform_file_processed file)));
wenzelm@12778
  1107
wenzelm@12778
  1108
val inform_file_retractedP =
wenzelm@12778
  1109
  OuterSyntax.improper_command "ProofGeneral.inform_file_retracted" "(internal)" K.control
wenzelm@12778
  1110
    (P.name >> (Toplevel.no_timing oo
wenzelm@14902
  1111
      (fn file => Toplevel.imperative (fn () => inform_file_retracted file))));
wenzelm@12778
  1112
wenzelm@14725
  1113
val process_pgipP =
wenzelm@14725
  1114
  OuterSyntax.improper_command "ProofGeneral.process_pgip" "(internal)" K.control
wenzelm@14725
  1115
    (P.text >> (Toplevel.no_timing oo
wenzelm@14725
  1116
      (fn txt => Toplevel.imperative (fn () => process_pgip txt))));
wenzelm@14725
  1117
wenzelm@12778
  1118
fun init_outer_syntax () = OuterSyntax.add_parsers
wenzelm@14675
  1119
 [undoP, restartP, kill_proofP, context_thy_onlyP, try_context_thy_onlyP,
wenzelm@14725
  1120
  inform_file_processedP, inform_file_retractedP, process_pgipP];
wenzelm@12778
  1121
wenzelm@12778
  1122
end;
wenzelm@12778
  1123
wenzelm@12778
  1124
wenzelm@12778
  1125
(* init *)
wenzelm@12778
  1126
wenzelm@12778
  1127
val initialized = ref false;
wenzelm@12778
  1128
aspinall@15134
  1129
fun set_prompts true _ = ml_prompts "ML> " "ML# " 
aspinall@15134
  1130
  | set_prompts false true = ml_prompts "PGIP-ML>" "PGIP-ML# "
aspinall@15134
  1131
  | set_prompts false false = 
aspinall@15134
  1132
    ml_prompts ("> " ^ oct_char "372") ("- " ^ oct_char "373");
aspinall@15134
  1133
aspinall@15134
  1134
fun init_setup isar pgip =
wenzelm@12778
  1135
 (conditional (not (! initialized)) (fn () =>
wenzelm@12778
  1136
   (if isar then setmp warning_fn (K ()) init_outer_syntax () else ();
wenzelm@12778
  1137
    setup_xsymbols_output ();
aspinall@15134
  1138
    setup_pgml_output ();
wenzelm@12778
  1139
    setup_messages ();
wenzelm@12778
  1140
    setup_state ();
wenzelm@12778
  1141
    setup_thy_loader ();
wenzelm@13526
  1142
    setup_present_hook ();
wenzelm@12778
  1143
    set initialized; ()));
wenzelm@12778
  1144
  sync_thy_loader ();
wenzelm@12778
  1145
  print_mode := proof_generalN :: (! print_mode \ proof_generalN);
aspinall@15134
  1146
  if pgip then 
aspinall@15134
  1147
      print_mode := pgmlN :: (pgmlatomsN :: (! print_mode \ pgmlN \ pgmlatomsN)) 
aspinall@15134
  1148
    else ();
wenzelm@12778
  1149
  set quick_and_dirty;
wenzelm@12778
  1150
  ThmDeps.enable ();
aspinall@15134
  1151
  set_prompts isar pgip;
aspinall@15134
  1152
  pgip_active := pgip)
aspinall@15134
  1153
aspinall@15134
  1154
fun init isar = 
aspinall@15134
  1155
    (init_setup isar false;
aspinall@15134
  1156
     if isar then ((* da: this welcome is problematic: clashes with welcome
aspinall@15134
  1157
		      issued for PG anyway. 
aspinall@15134
  1158
		      welcome (); *)
aspinall@15134
  1159
		    Isar.sync_main ()) else isa_restart ());
aspinall@15134
  1160
aspinall@15134
  1161
fun init_pgip false = panic "Sorry, PGIP not supported for Isabelle/classic mode."
aspinall@15134
  1162
  | init_pgip true = (init_setup true true; pgip_toplevel());
wenzelm@12778
  1163
wenzelm@12778
  1164
wenzelm@12778
  1165
aspinall@15134
  1166
(** generate keyword classification elisp file **)
wenzelm@12778
  1167
wenzelm@12778
  1168
local
wenzelm@12778
  1169
wenzelm@12778
  1170
val regexp_meta = explode ".*+?[]^$";
aspinall@15134
  1171
val regexp_quote = 
aspinall@15134
  1172
    implode o map  (fn c => if c mem regexp_meta then "\\\\" ^ c else c)
aspinall@15134
  1173
    o explode;
wenzelm@12778
  1174
wenzelm@12778
  1175
fun defconst name strs =
wenzelm@12778
  1176
  "\n(defconst isar-keywords-" ^ name ^
wenzelm@12778
  1177
  "\n  '(" ^ space_implode "\n    " (map (quote o regexp_quote) strs) ^ "))\n";
wenzelm@12778
  1178
wenzelm@12778
  1179
fun make_elisp_commands commands kind =
aspinall@15134
  1180
  defconst kind (mapfilter 
aspinall@15134
  1181
		     (fn (c, _, k, _) => if k = kind then Some c else None) 
aspinall@15134
  1182
		     commands);
wenzelm@12778
  1183
wenzelm@12778
  1184
fun make_elisp_syntax (keywords, commands) =
wenzelm@12778
  1185
  ";;\n\
wenzelm@12778
  1186
  \;; Keyword classification tables for Isabelle/Isar.\n\
wenzelm@12778
  1187
  \;; This file was generated by " ^ Session.name () ^ " -- DO NOT EDIT!\n\
wenzelm@12778
  1188
  \;;\n\
wenzelm@12778
  1189
  \;; $" ^ "Id$\n\
wenzelm@12778
  1190
  \;;\n" ^
wenzelm@12778
  1191
  defconst "major" (map #1 commands) ^
aspinall@15134
  1192
  defconst "minor" (filter Syntax.is_identifier keywords) ^
wenzelm@12778
  1193
  implode (map (make_elisp_commands commands) OuterSyntax.Keyword.kinds) ^
wenzelm@12778
  1194
  "\n(provide 'isar-keywords)\n";
wenzelm@12778
  1195
wenzelm@12778
  1196
in
wenzelm@12778
  1197
wenzelm@12778
  1198
fun write_keywords s =
wenzelm@12778
  1199
  (init_outer_syntax ();
wenzelm@12778
  1200
    File.write (Path.unpack ("isar-keywords" ^ (if s = "" then "" else "-" ^ s) ^".el"))
aspinall@15134
  1201
      (make_elisp_syntax (OuterSyntax.dest_keywords (), 
aspinall@15134
  1202
			  OuterSyntax.dest_parsers ())));
wenzelm@12778
  1203
wenzelm@12778
  1204
end;
wenzelm@12778
  1205
aspinall@15134
  1206
end