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