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