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