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