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