src/Pure/proof_general.ML
author berghofe
Thu Apr 21 19:12:03 2005 +0200 (2005-04-21)
changeset 15797 a63605582573
parent 15629 4066f01f1beb
child 15801 d2f5ca3c048d
permissions -rw-r--r--
- Eliminated nodup_vars check.
- Unification and matching functions now check types of term variables / sorts
of type variables when applying a substitution.
- Thm.instantiate now takes (ctyp * ctyp) list instead of (indexname * ctyp) list
as argument, to allow for proper instantiation of theorems containing
type variables with same name but different sorts.
     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 	      getOpt (Option.map (single o (pair "refseq")) (!pgip_refseq), []) @
   183 	      getOpt (Option.map (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     List.app tell_file_loaded (ThyInfo.loaded_files name)
   399   else if action = ThyInfo.Outdate orelse action = ThyInfo.Remove then
   400     List.app 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 () = List.app (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 isSome (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 if_known_thy_no_warning f name = if ThyInfo.known_thy name then f name else ();
   438 
   439 val openfile_retract = 
   440     if_known_thy_no_warning ThyInfo.remove_thy o thy_name;
   441 
   442 fun proper_inform_file_processed file state =
   443   let val name = thy_name file in
   444     if Toplevel.is_toplevel state andalso ThyInfo.known_thy name then
   445      (ThyInfo.touch_child_thys name;
   446       transform_error ThyInfo.pretend_use_thy_only name handle ERROR_MESSAGE msg =>
   447        (warning msg; warning ("Failed to register theory: " ^ quote name);
   448         tell_file_retracted (Path.base (Path.unpack file))))
   449     else raise Toplevel.UNDEF
   450   end;
   451 
   452 fun vacuous_inform_file_processed file state =
   453  (warning ("No theory " ^ quote (thy_name file));
   454   tell_file_retracted (Path.base (Path.unpack file)));
   455 
   456 
   457 (* restart top-level loop (keeps most state information) *)
   458 
   459 local
   460 
   461 fun restart isar =
   462  (if isar then tell_clear_goals () else kill_goal ();
   463   tell_clear_response ();
   464   welcome ());
   465 
   466 in
   467 
   468 fun isa_restart () = restart false;
   469 fun isar_restart () = (sync_thy_loader (); restart true; raise Toplevel.RESTART);
   470 
   471 end;
   472 
   473 fun full_proofs true = proofs := 2
   474   | full_proofs false = proofs := 1;
   475 
   476 
   477 (* theorem dependency output *)
   478 
   479 local
   480 
   481 val spaces_quote = space_implode " " o map quote;
   482 
   483 fun thm_deps_message (thms, deps) = 
   484     if pgip() then
   485 	issue_pgips 
   486 	    [XML.element
   487 		 "metainforesponse"  (* FIXME: get thy name from info here? *)
   488 		 [("infotype", "isabelle_theorem_dependencies")]
   489 		 [XML.element "value" [("name", "thms")] [XML.text thms],
   490 		  XML.element "value" [("name", "deps")] [XML.text deps]]]
   491     else emacs_notify 
   492 	     ("Proof General, theorem dependencies of " 
   493 	      ^ thms ^ " are " ^ deps)
   494 
   495 
   496 fun tell_thm_deps ths =
   497   conditional (thm_depsN mem_string ! print_mode) (fn () =>
   498     let
   499       val names = map Thm.name_of_thm ths \ "";
   500       val deps = Symtab.keys (Library.foldl (uncurry Proofterm.thms_of_proof)
   501 				    (Symtab.empty, map Thm.proof_of ths)) \ "";
   502     in
   503       if null names orelse null deps then ()
   504       else thm_deps_message (spaces_quote names, spaces_quote deps)
   505     end);
   506 
   507 in
   508 
   509 fun setup_present_hook () =
   510   Present.add_hook (fn _ => fn res => tell_thm_deps (List.concat (map #2 res)));
   511 
   512 end;
   513 
   514 
   515 (*** Preferences ***)
   516 
   517 local
   518 val pgipnat        = XML.element "pgipint" [("min", "0")] [] 
   519 fun pgipnatmax max = XML.element "pgipint" [("min", "0"), 
   520 					    ("max", string_of_int max)] []
   521 val pgipbool       = XML.element "pgipbool" [] []
   522 
   523 fun withdefault f = (f(), f)
   524 in
   525 
   526 fun nat_option r = (pgipnat,
   527   withdefault (fn () => string_of_int (!r)),
   528   (fn s => (case Syntax.read_nat s of
   529        NONE => error ("nat_option: illegal value " ^ s)
   530      | SOME i => r := i)));
   531 
   532 fun bool_option r = (pgipbool,
   533   withdefault (fn () => Bool.toString (!r)),
   534   (fn "false" => r := false | "true" => r := true
   535     | x => error ("bool_option: illegal value" ^ x)));
   536 
   537 val proof_option = (pgipbool,
   538   withdefault (fn () => Bool.toString (!proofs >= 2)),
   539   (fn "false" => proofs := 1 | "true" => proofs := 2
   540     | x => error ("proof_option: illegal value" ^ x)));
   541 
   542 val thm_deps_option = (pgipbool,
   543   withdefault (fn () => Bool.toString (Output.has_mode "thm_deps")),
   544   (fn "false" => print_mode := ((!print_mode) \ "thm_deps")
   545     | "true" => print_mode := ("thm_deps" ins (!print_mode))
   546     | x => error ("thm_deps_option: illegal value " ^ x)));
   547 
   548 local 
   549     val pg_print_depth_val = ref 10
   550     fun pg_print_depth n = (print_depth n; pg_print_depth_val := n)
   551 in
   552 val print_depth_option = (pgipnat,
   553   withdefault (fn () => string_of_int (!pg_print_depth_val)),
   554   (fn s => (case Syntax.read_nat s of
   555        NONE => error ("print_depth_option: illegal value" ^ s)
   556      | SOME i => pg_print_depth i)))
   557 end
   558 
   559 val preferences = ref 
   560   [("Display",
   561     [("show-types", 
   562       ("Include types in display of Isabelle terms", 
   563        bool_option show_types)),
   564      ("show-sorts", 
   565       ("Include sorts in display of Isabelle terms", 
   566        bool_option show_sorts)),
   567      ("show-consts", 
   568       ("Show types of consts in Isabelle goal display",
   569        bool_option show_consts)),
   570      ("long-names", 
   571       ("Show fully qualified names in Isabelle terms", bool_option long_names)),
   572      ("show-brackets", 
   573       ("Show full bracketing in Isabelle terms",
   574        bool_option show_brackets)),
   575      ("show-main-goal", 
   576       ("Show main goal in proof state display", bool_option Proof.show_main_goal)),
   577      ("eta-contract", 
   578       ("Print terms eta-contracted",
   579        bool_option Syntax.eta_contract))]),
   580    ("Advanced Display",
   581     [("goals-limit", 
   582       ("Setting for maximum number of goals printed",
   583        nat_option goals_limit)),
   584      ("prems-limit", 
   585       ("Setting for maximum number of premises printed",
   586        nat_option ProofContext.prems_limit)),
   587      ("print-depth", 
   588       ("Setting for the ML print depth",
   589        print_depth_option)),
   590      ("show-var-qmarks",
   591       ("Show leading question mark of variable name",
   592        bool_option show_var_qmarks))]),
   593    ("Tracing",
   594     [("trace-simplifier", 
   595       ("Trace simplification rules.",
   596        bool_option trace_simp)),
   597      ("trace-rules", ("Trace application of the standard rules",
   598 		      bool_option trace_rules)),
   599      ("trace-unification", 
   600       ("Output error diagnostics during unification",
   601        bool_option Pattern.trace_unify_fail)),
   602      ("global-timing", 
   603       ("Whether to enable timing in Isabelle.",
   604        bool_option Output.timing))]),
   605    ("Proof", 
   606     [("quick-and-dirty", 
   607       ("Take a few (interactive-only) short cuts",
   608        bool_option quick_and_dirty)),
   609      ("full-proofs", 
   610       ("Record full proof objects internally",
   611        proof_option)),
   612      ("theorem-dependencies", 
   613        ("Track theorem dependencies within Proof General",
   614 	thm_deps_option)),
   615      ("skip-proofs", 
   616       ("Skip all proof scripts (interactive-only)",
   617        bool_option Toplevel.skip_proofs))])
   618    ];
   619 end
   620 
   621 (* Configuration: GUI config, proverinfo messages *)
   622 
   623 local
   624     val config_file = "~~/lib/ProofGeneral/pgip_isar.xml"
   625     val name_attr = pair "name"
   626     val version_attr = pair "version"
   627     val isabelle_www = "http://isabelle.in.tum.de/"
   628 in
   629 fun send_pgip_config () =
   630     let 
   631 	val path = Path.unpack config_file
   632 	val exists = File.exists path
   633 	val proverinfo = 
   634 	    XML.element "proverinfo"
   635               [("name",Session.name()), ("version", version),
   636 	       ("url", isabelle_www), ("filenameextns", ".thy;")]
   637 	    [XML.element "welcomemsg" [] [XML.text (Session.welcome())],
   638 	     XML.element "helpdoc" 
   639          (* NB: would be nice to generate/display docs from isatool
   640           doc, but that program may not be running on same machine;
   641           front end should be responsible for launching viewer, etc. *)
   642 		      [("name", "Isabelle/HOL Tutorial"),
   643 		       ("descr", "A Gentle Introduction to Isabelle/HOL"), 
   644 		       ("url",  "http://isabelle.in.tum.de/dist/Isabelle2004/doc/tutorial.pdf")]
   645 	      []]
   646     in
   647 	if exists then
   648 	    (issue_pgips [proverinfo]; issue_pgips [File.read path])
   649 	else panic ("PGIP configuration file " ^ config_file ^ " not found")
   650     end;
   651 end
   652 
   653 
   654 (* Reveal some information about prover state *)
   655 fun send_informguise (openfile, opentheory, openproofpos) =
   656     let val guisefile = 
   657 	    case openfile of SOME f => [XML.element "guisefile" 
   658 						    [("url",Url.pack (Url.File (Path.unpack f)))] []]
   659 			   | _ => []
   660 	val guisetheory = 
   661 	    case opentheory of SOME t => [XML.element "guisetheory" [("thyname", t)] []]
   662 			     | _ => []
   663 	val guiseproof = 
   664 	    case openproofpos of SOME i => [XML.element "guiseproof" [("proofpos", string_of_int i)] []]
   665 			       | _ => []
   666     in 
   667 	issue_pgips [XML.element "informguise" [] (guisefile @ guisetheory @ guiseproof)]
   668     end 
   669 
   670 
   671 (* PGIP identifier tables (prover objects). [incomplete] *)
   672 
   673 local
   674     val objtype_thy  = "theory"
   675     val objtype_thm  = "theorem"
   676     val objtype_term = "term"
   677     val objtype_type = "type"
   678 		       
   679     fun xml_idtable ty ctx ids = 
   680 	let
   681             fun ctx_attr (SOME c)= [("context", c)]
   682               | ctx_attr NONE    = []
   683 	    fun xmlid x = XML.element "identifier" [] [XML.text x];
   684 	in 
   685 	    XML.element "idtable" (("objtype", ty)::ctx_attr ctx)
   686 	                          (map xmlid ids)
   687 	end
   688 in
   689 
   690 fun setids t = issue_pgip "setids" [] t
   691 fun addids t = issue_pgip "addids" [] t
   692 fun delids t = issue_pgip "delids" [] t
   693 
   694 fun delallids ty = setids (xml_idtable ty NONE [])
   695 
   696 fun send_thy_idtable ctx thys = setids (xml_idtable objtype_thy ctx thys)
   697 fun clear_thy_idtable () = delallids objtype_thy
   698 
   699 fun send_thm_idtable ctx thy = 
   700     addids (xml_idtable objtype_thm ctx (map fst (PureThy.thms_of thy)));
   701 
   702 fun clear_thm_idtable () = delallids objtype_thm
   703 
   704 (* fun send_type_idtable thy = TODO, it's a bit low-level messy
   705    & maybe not so useful anyway *)
   706 	
   707 end
   708 
   709 (* Response to interface queries about known objects *)
   710 
   711 local
   712  val topthy = Toplevel.theory_of o Toplevel.get_state
   713  fun pthm thy name = print_thm (get_thm thy (name, NONE))
   714 
   715  fun idvalue tp nm = ("idvalue",[("objtype",tp),("name",nm)])
   716 in
   717 fun askids (NONE, SOME "theory")  = send_thy_idtable NONE (ThyInfo.names())
   718   | askids (NONE, NONE) =  send_thy_idtable NONE (ThyInfo.names())
   719                            (* only theories known in top context *)
   720   | askids (SOME thy, SOME "theory") = send_thy_idtable (SOME thy) (ThyInfo.get_preds thy)
   721   | askids (SOME thy, SOME "theorem") = send_thm_idtable (SOME thy) (ThyInfo.get_theory thy)
   722   | askids (SOME thy, NONE) = (send_thy_idtable (SOME thy) (ThyInfo.get_preds thy);
   723                                send_thm_idtable (SOME thy) (ThyInfo.get_theory thy)) 
   724   | askids (_, SOME ot) = error ("No objects of type "^(quote ot)^" are available here.")
   725 
   726 fun showid (_,        "theory", n) = 
   727     with_displaywrap (idvalue "theory" n) (fn ()=>(print_theory (ThyInfo.get_theory n)))
   728   | showid (SOME thy, "theorem", t) = 
   729     with_displaywrap (idvalue "theorem" t) (fn ()=>(pthm (ThyInfo.get_theory thy) t))
   730   | showid (NONE,     "theorem", t) = 
   731     with_displaywrap (idvalue "theorem" t) (fn ()=>pthm (topthy()) t)
   732   | showid (_, ot, _) = error ("Cannot show objects of type "^ot)
   733 
   734 end
   735 
   736 
   737 (** Parsing proof scripts without execution **)
   738 
   739 (* Notes.
   740    This is quite tricky, because 1) we need to put back whitespace which
   741    was removed during parsing so we can provide markup around commands;
   742    2) parsing is intertwined with execution in Isar so we have to repeat
   743    the parsing to extract interesting parts of commands.  The trace of
   744    tokens parsed which is now recorded in each transition (added by
   745    Markus June '04) helps do this, but the mechanism is still a bad mess.
   746    
   747    If we had proper parse trees it would be easy, although having a
   748    fixed type of trees might be tricky with Isar's extensible parser.
   749 
   750    Probably the best solution is to produce the meta-information at
   751    the same time as the parse, for each command, e.g. by recording a 
   752    list of (name,objtype) pairs which record the bindings created by 
   753    a command.  This would require changing the interfaces in 
   754    outer_syntax.ML (or providing new ones), 
   755 
   756     datatype metainfo = Binding of string * string  (* name, objtype *)
   757 
   758     val command_withmetainfo: string -> string -> string ->
   759       (token list -> 
   760        ((Toplevel.transition -> Toplevel.transition) * metainfo list) * 
   761        token list) -> parser
   762 
   763    We'd also like to render terms as they appear in output, but this
   764    will be difficult because inner syntax is extensible and we don't 
   765    have the correct syntax to hand when just doing outer parsing
   766    without execution.  A reasonable approximation could 
   767    perhaps be obtained by using the syntax of the current context.
   768    However, this would mean more mess trying to pick out terms, 
   769    so at this stage a more serious change to the Isar functions
   770    seems necessary.
   771 *)
   772 
   773 local
   774     fun markup_text str elt = [XML.element elt [] [XML.text str]]
   775     fun markup_text_attrs str elt attrs = [XML.element elt attrs [XML.text str]]
   776     fun empty elt = [XML.element elt [] []]
   777 
   778     fun whitespace str = XML.element "whitespace" [] [XML.text str]
   779 
   780     (* an extra token is needed to terminate the command *)
   781     val sync = OuterSyntax.scan "\\<^sync>";
   782 
   783     fun named_item_elt_with nameattr toks str elt nameP objtyp = 
   784 	let 
   785 	    val name = (fst (nameP (toks@sync)))
   786 			handle _ => (error ("Error occurred in name parser for " ^ elt ^ 
   787 					    "(objtype: " ^ objtyp ^ ")");
   788 				     "")
   789 				     
   790 	in 
   791 	    [XML.element elt 
   792 			 ((if name="" then [] else [(nameattr, name)])@
   793 			  (if objtyp="" then [] else [("objtype", objtyp)]))
   794 			 ([XML.text str])]
   795 	end
   796 
   797     val named_item_elt = named_item_elt_with "name"
   798     val thmnamed_item_elt = named_item_elt_with "thmname"
   799  
   800     fun parse_warning msg = warning ("script->PGIP markup parser: " ^ msg)
   801 
   802     (* FIXME: allow dynamic extensions to language here: we need a hook in
   803        outer_syntax.ML to reset this table. *)
   804 
   805     val keywords_classification_table = ref (NONE:(string Symtab.table) option)
   806 
   807     fun get_keywords_classification_table () = 
   808 	case (!keywords_classification_table) of
   809 	    SOME t => t
   810 	  | NONE => (let
   811 			 val tab = Library.foldl (fn (tab,(c,_,k,_))=>Symtab.update((c,k),tab)) 
   812 					 (Symtab.empty,OuterSyntax.dest_parsers())
   813 		     in (keywords_classification_table := SOME tab; tab) end)
   814 
   815 
   816 		    
   817     fun xmls_of_thy_begin (name,toks,str) = (* see isar_syn.ML/theoryP *)
   818 	let 
   819 	    val ((thyname,imports,files),_) = ThyHeader.args (toks@sync)
   820 	in 
   821 	    markup_text_attrs str "opentheory" 
   822 			      ([("thyname",thyname)] @
   823 			       (if imports=[] then [] else
   824 				[("parentnames", (space_implode ";" imports) ^ ";")]))
   825 	end 
   826 
   827     fun xmls_of_thy_decl (name,toks,str) = (* see isar_syn.ML/thy_decl cases  *)
   828 	let 
   829 	    (* NB: PGIP only deals with single name bindings at the moment;
   830 	       potentially we could markup grouped definitions several times but
   831 	       that might suggest the wrong structure to the editor?
   832 	       Better alternative would be to put naming closer around text,
   833 	       but to do that we'd be much better off modifying the real parser
   834 	       instead of reconstructing it here. *)
   835 
   836 	    val plain_items = (* no names, unimportant names, or too difficult *)
   837 		["defaultsort","arities","judgement","finalconsts",
   838 		 "syntax", "nonterminals", "translations",
   839 		 "global", "local", "hide",
   840 		 "ML_setup", "setup", "method_setup",
   841 		 "parse_ast_translation", "parse_translation", "print_translation",
   842 		 "typed_print_translation", "print_ast_translation", "token_translation",
   843 		 "oracle",
   844 		 "declare"]
   845 
   846 	    val plain_item   = markup_text str "theoryitem"
   847 	    val comment_item = markup_text str "litcomment"
   848 	    val named_item   = named_item_elt toks str "theoryitem"
   849 
   850 	    val opt_overloaded = P.opt_keyword "overloaded";
   851 
   852 	    val thmnameP = (* see isar_syn.ML/theoremsP *)
   853 		let 
   854 		    val name_facts = P.and_list1 ((P.opt_thm_name "=" --| P.xthms1) >> #1)
   855 		    val theoremsP = P.locale_target |-- name_facts >> (fn [] => "" | x::_ => x)
   856 		in 
   857 		    theoremsP
   858 		end
   859 	in 
   860 	    (* TODO: ideally we would like to render terms properly, just as they are
   861 	       in output. This implies using PGML for symbols and variables/atoms. 
   862 	       BUT it's rather tricky without having the correct concrete syntax to hand,
   863 	       and even if we did, we'd have to mess around here a whole lot more first
   864 	       to pick out the terms from the syntax. *)
   865 
   866 	    if (name mem plain_items) then plain_item
   867 	    else case name of
   868 		     "text"      => comment_item
   869 		   | "text_raw"  => comment_item
   870 		   | "typedecl"  => named_item (P.type_args |-- P.name) "type"
   871 		   | "types"     => named_item (P.type_args |-- P.name) "type"
   872 		   | "classes"   => named_item P.name "class"
   873 		   | "classrel"  => named_item P.name "class"
   874 		   | "consts"    => named_item (P.const >> #1) "term"
   875 		   | "axioms"    => named_item (P.spec_name >> (#1 o #1)) "theorem"
   876 		   | "defs"	 => named_item (opt_overloaded |-- P.spec_name >> (#1 o #1)) "theorem"
   877 		   | "constdefs" => named_item P.name (* FIXME: heavily simplified/wrong *) "term"
   878 		   | "theorems"  => named_item thmnameP "thmset"
   879 		   | "lemmas"    => named_item thmnameP "thmset"
   880 		   | "oracle"    => named_item P.name "oracle"
   881 		   | "locale"	 => named_item ((P.opt_keyword "open" >> not) |-- P.name) "locale"
   882 		   | _ => (parse_warning ("Unrecognized thy-decl command: " ^ name); plain_item)
   883 	end
   884 
   885     fun xmls_of_thy_goal (name,toks,str) = 
   886 	let 
   887 	    (* see isar_syn.ML/gen_theorem *)
   888          val statement = P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.propp);
   889 	 val general_statement =
   890 	    statement >> pair [] || Scan.repeat P.locale_elem_or_expr -- (P.$$$ "shows" |-- statement);
   891 	    
   892 	    val gen_theoremP =
   893 		P.locale_target -- Scan.optional (P.opt_thm_name ":" --|
   894                  Scan.ahead (P.locale_keyword || P.$$$ "shows")) ("", []) --
   895 				 general_statement >> (fn ((locale, a), (elems, concl)) => 
   896 							 fst a) (* a : (bstring * Args.src list) *)
   897 
   898 	    val nameP = P.locale_target |-- (Scan.optional ((P.opt_thm_name ":") >> #1) "")
   899 	    (* TODO: add preference values for attributes 
   900 	       val prefval = XML.element "prefval" [("name","thm-kind"),("value",name)]
   901 	    *)
   902 	in 
   903 	    (thmnamed_item_elt toks str "opengoal" nameP "") @
   904 	    (empty "openblock")
   905 	end
   906 
   907     fun xmls_of_qed (name,markup) = (case name of
   908       "sorry"         => markup "giveupgoal"
   909     | "oops"          => markup "postponegoal"
   910     | "done"          => markup "closegoal" 
   911     | "by"            => markup "closegoal"  (* nested or toplevel *)
   912     | "qed"           => markup "closegoal"  (* nested or toplevel *)
   913     | "."	      => markup "closegoal"  (* nested or toplevel *)
   914     | ".."	      => markup "closegoal"  (* nested or toplevel *)
   915     | other => (* default to closegoal: may be wrong for extns *)
   916       (parse_warning ("Unrecognized qed command: " ^ quote other); markup "closegoal"))
   917 	@ (empty "closeblock")
   918 
   919     fun xmls_of_kind kind (name,toks,str) = 
   920     let val markup = markup_text str in 
   921     case kind of
   922       "control"        => markup "badcmd"
   923     | "diag"           => markup "spuriouscmd"
   924     (* theory/files *)
   925     | "theory-begin"   => xmls_of_thy_begin (name,toks,str)
   926     | "theory-decl"    => xmls_of_thy_decl (name,toks,str)
   927     | "theory-heading" => markup "litcomment"
   928     | "theory-script"  => markup "theorystep"
   929     | "theory-end"     => markup "closetheory"
   930     (* proof control *)
   931     | "theory-goal"    => xmls_of_thy_goal (name,toks,str)
   932     | "proof-heading"  => markup "litcomment"
   933     | "proof-goal"     => (markup "opengoal") @ (empty "openblock")  (* nested proof: have, show, ... *)
   934     | "proof-block"    => markup "proofstep" (* context-shift: proof, next; really "newgoal" *)
   935     | "proof-open"     => (empty "openblock") @ (markup "proofstep")
   936     | "proof-close"    => (markup "proofstep") @ (empty "closeblock")
   937     | "proof-script"   => markup "proofstep"
   938     | "proof-chain"    => markup "proofstep"
   939     | "proof-decl"     => markup "proofstep"
   940     | "proof-asm"      => markup "proofstep"
   941     | "proof-asm-goal" => (markup "opengoal") @ (empty "openblock")  (* nested proof: obtain *)
   942     | "qed"            => xmls_of_qed (name,markup)
   943     | "qed-block"      => xmls_of_qed (name,markup)
   944     | "qed-global"     => xmls_of_qed (name,markup)
   945     | other => (* default for anything else is "spuriouscmd", ignored for undo. *)
   946       (parse_warning ("Internal inconsistency, unrecognized keyword kind: " ^ quote other);
   947        markup "spuriouscmd")
   948     end 
   949 in
   950 
   951 fun xmls_of_transition (name,str,toks) = 
   952    let 
   953        val classification = Symtab.lookup (get_keywords_classification_table(),name)
   954    in case classification of
   955 	  SOME k => (xmls_of_kind k (name,toks,str))
   956 	| NONE => (* an uncategorized keyword ignored for undo (maybe wrong) *)
   957 	  (parse_warning ("Uncategorized command found: " ^ name ^ " -- using spuriouscmd");
   958 	   markup_text str "spuriouscmd")
   959    end 
   960 
   961 fun markup_toks [] _ = []
   962   | markup_toks toks x = markup_text (implode (map OuterLex.unparse toks)) x
   963 
   964 fun markup_comment_whs [] = []
   965   | markup_comment_whs (toks as t::ts) = (* this would be a lot neater if we could match on toks! *)
   966     let 
   967 	val (prewhs,rest) = take_prefix (OuterLex.is_kind OuterLex.Space) toks
   968     in 
   969 	if (prewhs <> []) then
   970 	    whitespace (implode (map OuterLex.unparse prewhs))
   971 	    :: (markup_comment_whs rest)
   972 	else 
   973 	    (markup_text (OuterLex.unparse t) "comment") @
   974 	    (markup_comment_whs ts)
   975     end
   976 
   977 fun xmls_pre_cmd [] = ([],[])
   978   | xmls_pre_cmd toks = 
   979     let 
   980 	(* an extra token is needed to terminate the command *)
   981 	val sync = OuterSyntax.scan "\\<^sync>";
   982 	val spaceP = Scan.bulk (Scan.one (fn t =>not (OuterLex.is_proper t)) >> OuterLex.val_of) >> implode
   983 	val text_with_whs = 
   984 	    ((spaceP || Scan.succeed "") --
   985 	     (P.short_ident || P.long_ident || P.sym_ident || P.string || P.number || P.verbatim) >> op^)
   986 	     -- (spaceP || Scan.succeed "") >> op^
   987 	val (prewhs,rest1) = take_prefix (not o OuterLex.is_proper) (toks@sync)
   988         (* NB: this collapses  litcomment,(litcomment|whitespace)* to a single litcomment *)
   989 	val (_,rest2) = (Scan.bulk (P.$$$ "--" |-- text_with_whs) >> implode || Scan.succeed "") rest1
   990 	val (postwhs,rest3) = take_prefix (not o OuterLex.is_proper) rest2
   991     in
   992 	((markup_comment_whs prewhs) @
   993 	 (if (length rest2 = length rest1)  then []
   994 	  else markup_text (implode 
   995 				(map OuterLex.unparse (Library.take (length rest1 - length rest2, rest1))))
   996 	       "litcomment") @
   997 	 (markup_comment_whs postwhs),
   998 	 Library.take (length rest3 - 1,rest3))
   999     end
  1000 
  1001 fun xmls_of_impropers toks = 
  1002     let 
  1003 	val (xmls,rest) = xmls_pre_cmd toks
  1004     in
  1005 	xmls @ (markup_toks rest "unparseable")
  1006     end
  1007     
  1008 fun markup_unparseable str = markup_text str "unparseable" 
  1009 
  1010 end
  1011 
  1012 
  1013 local
  1014     (* we have to weave together the whitespace/comments with proper tokens 
  1015        to reconstruct the input. *)
  1016     (* TODO: see if duplicating isar_output/parse_thy can help here *)
  1017 
  1018     fun match_tokens ([],us,vs) = (rev vs,us)  (* used, unused *)
  1019       | match_tokens (t::ts,w::ws,vs) = 
  1020 	if (t = w) then match_tokens (ts,ws,w::vs)
  1021 	else match_tokens (t::ts,ws,w::vs)
  1022       | match_tokens _ = error ("match_tokens: mismatched input parse")
  1023 in
  1024     fun xmls_of_str str =
  1025     let 
  1026        (* parsing:   See outer_syntax.ML/toplevel_source *)
  1027        fun parse_loop ([],[],xmls) = xmls
  1028 	 | parse_loop ([],itoks,xmls) = xmls @ (xmls_of_impropers itoks)
  1029 	 | parse_loop ((nm,toks,_)::trs,itoks,xmls) =
  1030 	   let 
  1031 	       (* first proper token after whitespace/litcomment/whitespace is command *)
  1032 	       val (xmls_pre_cmd,cmditoks') = xmls_pre_cmd itoks
  1033 	       val (cmdtok,itoks') = case cmditoks' of x::xs => (x,xs)
  1034 						     | _ => error("proof_general/parse_loop impossible") 
  1035 	       val (utoks,itoks'') = match_tokens (toks,itoks',[])
  1036                (* FIXME: should take trailing [w/s+] semicolon too in utoks *)
  1037 
  1038 	       val str = implode (map OuterLex.unparse (cmdtok::utoks))
  1039 
  1040 	       val xmls_tr  = xmls_of_transition (nm,str,toks)
  1041 	   in
  1042 	       parse_loop(trs,itoks'',xmls @ xmls_pre_cmd @ xmls_tr)
  1043 	   end
  1044     in
  1045 	(let val toks = OuterSyntax.scan str
  1046 	 in 
  1047 	     parse_loop (OuterSyntax.read toks, toks, [])
  1048 	 end)
  1049  	   handle _ => markup_unparseable str
  1050     end
  1051 
  1052 
  1053 fun parsescript str attrs = 
  1054     let 
  1055 	val _ = start_delay_msgs ()  (* accumulate error messages to put inside parseresult *)
  1056 	val xmls = xmls_of_str str
  1057         val errs = end_delayed_msgs ()
  1058      in 
  1059 	issue_pgips [XML.element "parseresult" attrs (errs@xmls)]
  1060     end
  1061 end
  1062 
  1063 
  1064 
  1065 (**** PGIP:  Isabelle -> Interface ****)
  1066 
  1067 val isabelle_pgml_version_supported = "1.0"; 
  1068 val isabelle_pgip_version_supported = "2.0"
  1069 
  1070 fun usespgip () = 
  1071     issue_pgipe "usespgip" [("version", isabelle_pgip_version_supported)];
  1072 
  1073 fun usespgml () = 
  1074     issue_pgipe "usespgml" [("version", isabelle_pgml_version_supported)];
  1075 
  1076 fun hasprefs () = 
  1077     List.app (fn (prefcat, prefs) =>
  1078 	    issue_pgips [XML.element "hasprefs" [("prefcategory",prefcat)]
  1079 		 (map (fn (name, (descr, (ty, (default,_),_))) => 
  1080 		       XML.element "haspref" [("name", name), 
  1081 					      ("descr", descr), 
  1082 					      ("default", default)]
  1083 		       [ty]) prefs)]) (!preferences);
  1084 
  1085 fun allprefs () = Library.foldl (op @) ([], map snd (!preferences))
  1086 	
  1087 fun setpref name value = 
  1088     (case assoc (allprefs(), name) of
  1089 	 NONE => warning ("Unknown pref: " ^ quote name)
  1090        | SOME (_, (_, _, set)) => set value);
  1091 
  1092 fun getpref name = 
  1093     (case assoc (allprefs(), name) of
  1094 	 NONE => warning ("Unknown pref: " ^ quote name)
  1095        | SOME (_, (_, (_,get), _)) => 
  1096 	   issue_pgip "prefval" [("name", name)] (get ()));
  1097 
  1098 
  1099 
  1100 
  1101 
  1102 (**** PGIP:  Interface -> Isabelle/Isar ****)
  1103 
  1104 exception PGIP of string;
  1105 exception PGIP_QUIT;
  1106 
  1107 (* Sending commands to Isar *)
  1108 
  1109 fun isarcmd s = 
  1110     s |> OuterSyntax.scan |> OuterSyntax.read 
  1111       |> map (Toplevel.position (Position.name "PGIP message") o #3) |> Toplevel.>>>;
  1112 
  1113 fun xmltext ((XML.Text text)::ts) = text ^ (xmltext ts)
  1114   | xmltext [] = ""
  1115   | xmltext _ = raise PGIP "Expected text (PCDATA/CDATA)"
  1116 			
  1117 fun isarscript xmls = isarcmd (xmltext xmls)   (* send a script command *)
  1118 
  1119 
  1120 (* load an arbitrary (.thy or .ML) file *)
  1121 
  1122 fun use_thy_or_ml_file file = 
  1123     let
  1124 	val (path,extn) = Path.split_ext (Path.unpack file)
  1125     in
  1126 	case extn of
  1127 	    "" => isarcmd ("use_thy " ^ (quote (Path.pack path)))
  1128 	  | "thy" => isarcmd ("use_thy " ^ (quote (Path.pack path)))
  1129 	  | "ML" => isarcmd ("use " ^ quote file)
  1130 	  (* instead of error we could guess theory? *)
  1131 	  | other => error ("Don't know how to read a file with extension " ^ other)
  1132     end  
  1133 
  1134 
  1135 (* Proof control commands *)
  1136 
  1137 local
  1138   fun xmlattro attr attrs = assoc(attrs,attr)
  1139 
  1140   fun xmlattr attr attrs = 
  1141       (case xmlattro attr attrs of 
  1142 	   SOME value => value 
  1143 	 | NONE => raise PGIP ("Missing attribute: " ^ attr))
  1144 
  1145   val thyname_attro = xmlattro "thyname"
  1146   val thyname_attr = xmlattr "thyname"
  1147   val objtype_attro = xmlattro "objtype"
  1148   val objtype_attr = xmlattr "objtype"
  1149   val name_attr = xmlattr "name"
  1150   val dirname_attr = xmlattr "dir"
  1151   fun comment x = "(* " ^ x ^ " *)"
  1152 
  1153   fun localfile_of_url url = (* only handle file:/// or file://localhost/ *)
  1154       case Url.unpack url of
  1155 	  (Url.File path) => File.sysify_path path
  1156 	| _ => error ("Cannot access non-local URL " ^ url)
  1157 
  1158   val fileurl_of = localfile_of_url o (xmlattr "url")
  1159 
  1160   val topthy = Toplevel.theory_of o Toplevel.get_state
  1161   val topthy_name = PureThy.get_name o topthy
  1162 
  1163   val currently_open_file = ref (NONE : string option)
  1164 
  1165   val topnode = Toplevel.node_of o Toplevel.get_state
  1166   fun topproofpos () = (case topnode() of Toplevel.Proof ph => SOME(ProofHistory.position ph) 
  1167 					| _ => NONE) handle Toplevel.UNDEF => NONE
  1168 in
  1169 
  1170 fun process_pgip_element pgipxml = (case pgipxml of 
  1171   (XML.Text t) => warning ("Ignored text in PGIP packet: \n" ^ t)
  1172 | (xml as (XML.Elem (elem, attrs, data))) => 
  1173   (case elem of
  1174        (* protocol config *)
  1175        "askpgip"  	=> (pgip_emacs_compatibility_flag:=false; (* PG>=3.6 or other PGIP interface *)
  1176 			    usespgip (); send_pgip_config ())
  1177      | "askpgml"  	=> usespgml ()
  1178      (* proverconfig *)
  1179      | "askprefs" 	=> hasprefs ()
  1180      | "getpref"  	=> getpref (name_attr attrs)
  1181      | "setpref"  	=> setpref (name_attr attrs) (xmltext data)
  1182      (* provercontrol *)
  1183      | "proverinit" 	=> isar_restart ()
  1184      | "proverexit" 	=> isarcmd "quit"
  1185      | "startquiet" 	=> isarcmd "disable_pr"
  1186      | "stopquiet"  	=> isarcmd "enable_pr"
  1187      | "pgmlsymbolson"   => (print_mode := !print_mode @ ["xsymbols"])
  1188      | "pgmlsymbolsoff"  => (print_mode := (!print_mode \ "xsymbols"))
  1189      (* properproofcmd: proper commands which belong in script *)
  1190      (* FIXME: next ten are by Eclipse interface, can be removed in favour of dostep *)
  1191      (* NB: Isar doesn't make lemma name of goal accessible during proof *)
  1192      | "opengoal"       => isarscript data
  1193      | "proofstep"      => isarscript data
  1194      | "closegoal"      => isarscript data
  1195      | "giveupgoal"     => isarscript data
  1196      | "postponegoal"   => isarscript data
  1197      | "comment"	=> isarscript data  (* NB: should be ignored, but process anyway *)
  1198      | "whitespace"	=> isarscript data  (* NB: should be ignored, but process anyway *)
  1199      | "litcomment"     => isarscript data
  1200      | "spuriouscmd"    => isarscript data
  1201      | "badcmd"		=> isarscript data
  1202      (* improperproofcmd: improper commands which *do not* belong in script *)
  1203      | "dostep"         => isarscript data
  1204      | "undostep"       => isarcmd "undos_proof 1"
  1205      | "redostep"       => isarcmd "redo"
  1206      | "abortgoal"      => isarcmd "ProofGeneral.kill_proof"  
  1207      | "forget"         => error "Not implemented" 
  1208      | "restoregoal"    => error "Not implemented"  (* could just treat as forget? *)
  1209      (* proofctxt: improper commands *)
  1210      | "askids"         => askids (thyname_attro attrs, objtype_attro attrs)
  1211      | "showid"	        => showid (thyname_attro attrs, objtype_attr attrs, name_attr attrs)
  1212      | "askguise"	=> send_informguise (!currently_open_file,
  1213 					     SOME (topthy_name()) handle Toplevel.UNDEF => NONE,
  1214 					     topproofpos())
  1215      | "parsescript"    => parsescript (xmltext data) attrs (* just pass back attrs unchanged *)
  1216      | "showproofstate" => isarcmd "pr"
  1217      | "showctxt"       => isarcmd "print_theory"   (* more useful than print_context *)
  1218      | "searchtheorems" => isarcmd ("thms_containing " ^ (xmltext data))
  1219      | "setlinewidth"   => isarcmd ("pretty_setmargin " ^ (xmltext data))
  1220      | "viewdoc"	=> isarcmd ("print_" ^ (xmltext data)) (* FIXME: isatool doc? *)
  1221      (* properfilecmd: proper theory-level script commands *)
  1222      (* FIXME: next three are sent by Eclipse, can be removed in favour of doitem *)
  1223      | "opentheory"     => isarscript data
  1224      | "theoryitem"     => isarscript data
  1225      | "closetheory"    => let 
  1226 			      val thyname = topthy_name()
  1227 			   in (isarscript data;
  1228 			       writeln ("Theory \""^thyname^"\" completed."))
  1229 			   end
  1230      (* improperfilecmd: theory-level commands not in script *)
  1231      | "doitem"         => isarscript data
  1232      | "undoitem"       => isarcmd "ProofGeneral.undo"
  1233      | "redoitem"       => isarcmd "ProofGeneral.redo"
  1234      | "aborttheory"    => isarcmd ("init_toplevel")
  1235      | "retracttheory"  => isarcmd ("kill_thy " ^ (quote (thyname_attr attrs)))
  1236      | "loadfile"       => use_thy_or_ml_file (fileurl_of attrs)
  1237      | "openfile"       => (openfile_retract (fileurl_of attrs);
  1238 			    currently_open_file := SOME (fileurl_of attrs))
  1239      | "closefile"      => (case !currently_open_file of 
  1240 				SOME f => (inform_file_processed f;
  1241 					   currently_open_file := NONE)
  1242 			      | NONE => raise PGIP ("closefile when no file is open!"))
  1243      | "abortfile"      => (currently_open_file := NONE) (* perhaps error for no file open *)
  1244      | "changecwd"      => ThyLoad.add_path (dirname_attr attrs)
  1245      | "systemcmd"	=> isarscript data
  1246      (* unofficial command for debugging *)
  1247      | "quitpgip" => raise PGIP_QUIT  
  1248      | _ => raise PGIP ("Unrecognized PGIP element: " ^ elem)))
  1249 
  1250 fun process_pgip_tree xml = 
  1251     (pgip_refseq := NONE; 
  1252      pgip_refid := NONE;
  1253      (case xml of
  1254 	  XML.Elem ("pgip", attrs, pgips) => 
  1255 	  (let 
  1256 	       val class = xmlattr "class" attrs
  1257 	       val _ = (pgip_refseq := xmlattro "seq" attrs;
  1258 			pgip_refid :=  xmlattro "id" attrs)
  1259 	   in  
  1260 	       if (class = "pa") then
  1261 		   List.app process_pgip_element pgips
  1262 	       else 
  1263 		   raise PGIP "PGIP packet for me should have class=\"pa\""
  1264 	   end)
  1265 	| _ => raise PGIP "Invalid PGIP packet received") 
  1266      handle (PGIP msg) => 
  1267 	    (error (msg ^ "\nPGIP error occured in XML text below:\n" ^ 
  1268 		    (XML.string_of_tree xml))))
  1269 
  1270 val process_pgip = process_pgip_tree o XML.tree_of_string;
  1271 
  1272 end
  1273 
  1274 
  1275 
  1276 
  1277 (* PGIP loop: process PGIP input only *)
  1278 
  1279 local  
  1280 
  1281 exception XML_PARSE
  1282 
  1283 fun loop src : unit =
  1284     let 
  1285 	val _ = issue_pgipe "ready" []
  1286 	val pgipo = (Source.get_single src) 
  1287 			handle e => raise XML_PARSE
  1288     in
  1289 	case pgipo of  
  1290 	     NONE  => ()
  1291 	   | SOME (pgip,src') =>  
  1292 	     ((process_pgip_tree pgip); loop src') handle e => handler (e,SOME src')
  1293     end handle e => handler (e,SOME src)  (* i.e. error in ready/XML parse *)
  1294 
  1295 and handler (e,srco) = 
  1296     case (e,srco) of
  1297         (XML_PARSE,SOME src) => 
  1298 	(* (!error_fn "Invalid XML input, aborting"; ()) NB: loop OK for tty, but want exit on EOF *)
  1299          panic "Invalid XML input, aborting"
  1300       | (PGIP_QUIT,_) => ()
  1301       | (ERROR,SOME src) => loop src (* message already given *)
  1302       | (Interrupt,SOME src) => (!error_fn "Interrupt during PGIP processing"; loop src)
  1303       | (Toplevel.UNDEF,SOME src) => (error "No working context defined"; loop src) (* usually *)
  1304       | (e,SOME src) => (error (Toplevel.exn_message e); loop src)
  1305       | (_,NONE) => ()
  1306 in
  1307   (* NB: simple tty for now; later might read from other tty-style sources (e.g. sockets). *)
  1308 
  1309   val xmlP = XML.scan_comment_whspc |-- XML.parse_elem >> single
  1310 
  1311   val tty_src = Source.set_prompt "" (Source.source Symbol.stopper xmlP NONE Source.tty)
  1312 
  1313   val pgip_toplevel =  loop 
  1314 end
  1315 
  1316 
  1317 (* additional outer syntax for Isar *)
  1318 
  1319 local structure P = OuterParse and K = OuterSyntax.Keyword in
  1320 
  1321 val undoP = (* undo without output *)
  1322   OuterSyntax.improper_command "ProofGeneral.undo" "(internal)" K.control
  1323     (Scan.succeed (Toplevel.no_timing o IsarCmd.undo));
  1324 
  1325 val redoP = (* redo without output *)
  1326   OuterSyntax.improper_command "ProofGeneral.redo" "(internal)" K.control
  1327     (Scan.succeed (Toplevel.no_timing o IsarCmd.redo));
  1328 
  1329 val context_thy_onlyP =
  1330   OuterSyntax.improper_command "ProofGeneral.context_thy_only" "(internal)" K.control
  1331     (P.name >> (Toplevel.no_timing oo IsarThy.init_context update_thy_only));
  1332 
  1333 val try_context_thy_onlyP =
  1334   OuterSyntax.improper_command "ProofGeneral.try_context_thy_only" "(internal)" K.control
  1335     (P.name >> (Toplevel.no_timing oo
  1336       (Toplevel.imperative (K ()) oo IsarThy.init_context try_update_thy_only)));
  1337 
  1338 val restartP =
  1339   OuterSyntax.improper_command "ProofGeneral.restart" "(internal)" K.control
  1340     (P.opt_unit >> (Toplevel.no_timing oo K (Toplevel.imperative isar_restart)));
  1341 
  1342 val kill_proofP =
  1343   OuterSyntax.improper_command "ProofGeneral.kill_proof" "(internal)" K.control
  1344     (Scan.succeed (Toplevel.no_timing o IsarCmd.kill_proof_notify tell_clear_goals));
  1345 
  1346 val inform_file_processedP =
  1347   OuterSyntax.improper_command "ProofGeneral.inform_file_processed" "(internal)" K.control
  1348     (P.name >> (fn file => Toplevel.no_timing o
  1349       Toplevel.keep (vacuous_inform_file_processed file) o
  1350       Toplevel.kill o
  1351       Toplevel.keep (proper_inform_file_processed file)));
  1352 
  1353 val inform_file_retractedP =
  1354   OuterSyntax.improper_command "ProofGeneral.inform_file_retracted" "(internal)" K.control
  1355     (P.name >> (Toplevel.no_timing oo
  1356       (fn file => Toplevel.imperative (fn () => inform_file_retracted file))));
  1357 
  1358 val process_pgipP =
  1359   OuterSyntax.improper_command "ProofGeneral.process_pgip" "(internal)" K.control
  1360     (P.text >> (Toplevel.no_timing oo
  1361       (fn txt => Toplevel.imperative (fn () => process_pgip txt))));
  1362 
  1363 fun init_outer_syntax () = OuterSyntax.add_parsers
  1364  [undoP, redoP, restartP, kill_proofP, context_thy_onlyP, try_context_thy_onlyP,
  1365   inform_file_processedP, inform_file_retractedP, process_pgipP];
  1366 
  1367 end;
  1368 
  1369 
  1370 (* init *)
  1371 
  1372 val initialized = ref false;
  1373 
  1374 fun set_prompts true _ = ml_prompts "ML> " "ML# " 
  1375   | set_prompts false true = ml_prompts "PGIP-ML>" "PGIP-ML# "
  1376   | set_prompts false false = 
  1377     ml_prompts ("> " ^ oct_char "372") ("- " ^ oct_char "373");
  1378 
  1379 fun init_setup isar pgip =
  1380  (conditional (not (! initialized)) (fn () =>
  1381    (if isar then setmp warning_fn (K ()) init_outer_syntax () else ();
  1382     setup_xsymbols_output ();
  1383     setup_pgml_output ();
  1384     setup_messages ();
  1385     setup_state ();
  1386     setup_thy_loader ();
  1387     setup_present_hook ();
  1388     set initialized; ()));
  1389   sync_thy_loader ();
  1390   print_mode := proof_generalN :: (! print_mode \ proof_generalN);
  1391   if pgip then 
  1392       print_mode := pgmlN :: (pgmlatomsN :: (! print_mode \ pgmlN \ pgmlatomsN)) 
  1393     else 
  1394 	pgip_emacs_compatibility_flag := true;  (* assume this for PG <3.6 compatibility *)
  1395   set quick_and_dirty;
  1396   ThmDeps.enable ();
  1397   set_prompts isar pgip;
  1398   pgip_active := pgip)
  1399 
  1400 fun init isar = 
  1401     (init_setup isar false;
  1402      if isar then ((* da: this welcome is problematic: clashes with welcome
  1403 		      issued for PG anyway. 
  1404 		      welcome (); *)
  1405 		    Isar.sync_main ()) else isa_restart ());
  1406 
  1407 fun init_pgip false = panic "Sorry, PGIP not supported for Isabelle/classic mode."
  1408   | init_pgip true = (init_setup true true; 
  1409 		      pgip_toplevel tty_src);
  1410 
  1411 
  1412 
  1413 (** generate keyword classification elisp file **)
  1414 
  1415 local
  1416 
  1417 val regexp_meta = explode ".*+?[]^$";
  1418 val regexp_quote = 
  1419     implode o map  (fn c => if c mem regexp_meta then "\\\\" ^ c else c)
  1420     o explode;
  1421 
  1422 fun defconst name strs =
  1423   "\n(defconst isar-keywords-" ^ name ^
  1424   "\n  '(" ^ space_implode "\n    " (map (quote o regexp_quote) strs) ^ "))\n";
  1425 
  1426 fun make_elisp_commands commands kind =
  1427   defconst kind (List.mapPartial 
  1428 		     (fn (c, _, k, _) => if k = kind then SOME c else NONE) 
  1429 		     commands);
  1430 
  1431 fun make_elisp_syntax (keywords, commands) =
  1432   ";;\n\
  1433   \;; Keyword classification tables for Isabelle/Isar.\n\
  1434   \;; This file was generated by " ^ Session.name () ^ " -- DO NOT EDIT!\n\
  1435   \;;\n\
  1436   \;; $" ^ "Id$\n\
  1437   \;;\n" ^
  1438   defconst "major" (map #1 commands) ^
  1439   defconst "minor" (List.filter Syntax.is_identifier keywords) ^
  1440   implode (map (make_elisp_commands commands) OuterSyntax.Keyword.kinds) ^
  1441   "\n(provide 'isar-keywords)\n";
  1442 
  1443 in
  1444 
  1445 fun write_keywords s =
  1446   (init_outer_syntax ();
  1447     File.write (Path.unpack ("isar-keywords" ^ (if s = "" then "" else "-" ^ s) ^".el"))
  1448       (make_elisp_syntax (OuterSyntax.dest_keywords (), 
  1449 			  OuterSyntax.dest_parsers ())));
  1450 
  1451 end;
  1452 
  1453 end