minor tuning;
authorwenzelm
Fri Dec 29 18:25:46 2006 +0100 (2006-12-29)
changeset 21940fbd068dd4d29
parent 21939 9b772ac66830
child 21941 62dd79056d70
minor tuning;
src/Pure/ProofGeneral/pgip_input.ML
src/Pure/ProofGeneral/pgip_isabelle.ML
src/Pure/ProofGeneral/pgip_output.ML
src/Pure/ProofGeneral/pgip_tests.ML
src/Pure/ProofGeneral/pgip_types.ML
src/Pure/ProofGeneral/preferences.ML
src/Pure/ProofGeneral/proof_general_emacs.ML
src/Pure/ProofGeneral/proof_general_pgip.ML
src/Pure/proof_general.ML
     1.1 --- a/src/Pure/ProofGeneral/pgip_input.ML	Fri Dec 29 18:25:45 2006 +0100
     1.2 +++ b/src/Pure/ProofGeneral/pgip_input.ML	Fri Dec 29 18:25:46 2006 +0100
     1.3 @@ -2,7 +2,7 @@
     1.4      ID:         $Id$
     1.5      Author:     David Aspinall
     1.6  
     1.7 -PGIP abstraction: input commands
     1.8 +PGIP abstraction: input commands.
     1.9  *)
    1.10  
    1.11  signature PGIPINPUT =
    1.12 @@ -146,7 +146,7 @@
    1.13      val times_attr = read_pgipnat o (get_attr_dflt "times" "1")
    1.14      val prefcat_attr = get_attr_opt "prefcategory"
    1.15  
    1.16 -    fun xmltext ((XML.Text text)::ts) = text ^ (xmltext ts)
    1.17 +    fun xmltext (XML.Text text :: ts) = text ^ xmltext ts
    1.18        | xmltext [] = ""
    1.19        | xmltext _ = raise PGIP "Expected text (PCDATA/CDATA)"
    1.20  
     2.1 --- a/src/Pure/ProofGeneral/pgip_isabelle.ML	Fri Dec 29 18:25:45 2006 +0100
     2.2 +++ b/src/Pure/ProofGeneral/pgip_isabelle.ML	Fri Dec 29 18:25:46 2006 +0100
     2.3 @@ -2,7 +2,7 @@
     2.4      ID:         $Id$
     2.5      Author:     David Aspinall
     2.6  
     2.7 -Prover-side PGIP abstraction: Isabelle configuration
     2.8 +Prover-side PGIP abstraction: Isabelle configuration.
     2.9  *)
    2.10  
    2.11  signature PGIP_ISABELLE =
     3.1 --- a/src/Pure/ProofGeneral/pgip_output.ML	Fri Dec 29 18:25:45 2006 +0100
     3.2 +++ b/src/Pure/ProofGeneral/pgip_output.ML	Fri Dec 29 18:25:46 2006 +0100
     3.3 @@ -2,7 +2,7 @@
     3.4      ID:         $Id$
     3.5      Author:     David Aspinall
     3.6  
     3.7 -PGIP abstraction: output commands
     3.8 +PGIP abstraction: output commands.
     3.9  *)
    3.10  
    3.11  signature PGIPOUTPUT =
    3.12 @@ -110,7 +110,7 @@
    3.13      let
    3.14          val area = #area vs
    3.15      in
    3.16 -        XML.Elem ("cleardisplay", (attrs_of_displayarea area), [])
    3.17 +        XML.Elem ("cleardisplay", attrs_of_displayarea area, [])
    3.18      end
    3.19  
    3.20  fun normalresponse (Normalresponse vs) =
    3.21 @@ -121,9 +121,9 @@
    3.22          val content = #content vs
    3.23      in
    3.24          XML.Elem ("normalresponse", 
    3.25 -                 (attrs_of_displayarea area) @
    3.26 +                 attrs_of_displayarea area @
    3.27                   (if urgent then attr "urgent" "true" else []) @
    3.28 -                 (attrs_of_messagecategory messagecategory),
    3.29 +                 attrs_of_messagecategory messagecategory,
    3.30                   content)
    3.31      end
    3.32  
    3.33 @@ -135,9 +135,9 @@
    3.34          val content = #content vs
    3.35      in
    3.36          XML.Elem ("errorresponse",
    3.37 -                 (the_default [] (Option.map attrs_of_displayarea area)) @
    3.38 -                 (attrs_of_fatality fatality) @
    3.39 -                 (the_default [] (Option.map attrs_of_location location)),
    3.40 +                 these (Option.map attrs_of_displayarea area) @
    3.41 +                 attrs_of_fatality fatality @
    3.42 +                 these (Option.map attrs_of_location location),
    3.43                   content)
    3.44      end
    3.45  
    3.46 @@ -267,7 +267,7 @@
    3.47          val errs = #errs vs
    3.48  	val xmldoc = PgipMarkup.output_doc doc
    3.49      in 
    3.50 -        XML.Elem("parseresult", attrs, errs@xmldoc)
    3.51 +        XML.Elem("parseresult", attrs, errs @ xmldoc)
    3.52      end
    3.53  
    3.54  fun acceptedpgipelems (Usespgip vs) = 
     4.1 --- a/src/Pure/ProofGeneral/pgip_tests.ML	Fri Dec 29 18:25:45 2006 +0100
     4.2 +++ b/src/Pure/ProofGeneral/pgip_tests.ML	Fri Dec 29 18:25:46 2006 +0100
     4.3 @@ -3,7 +3,7 @@
     4.4      Author:     David Aspinall
     4.5  
     4.6  A test suite for the PGIP abstraction code (in progress).
     4.7 -Run to provide some mild insurance against breakage in Isabelle/here.
     4.8 +Run to provide some mild insurance against breakage in Isabelle here.
     4.9  *)
    4.10  
    4.11  (** pgip_types.ML **)
    4.12 @@ -70,7 +70,7 @@
    4.13  open PgipInput;
    4.14  
    4.15  fun asseqi a b =
    4.16 -    if (input (e a))=b then ()
    4.17 +    if input (e a) = b then ()
    4.18      else error("PGIP test: expected two inputs to be equal, for input:\n" ^ a)
    4.19  
    4.20  in
    4.21 @@ -103,7 +103,7 @@
    4.22  open PgipMarkup
    4.23  open PgipParser
    4.24  fun asseqp a b =
    4.25 -    if (pgip_parser a)=b then ()
    4.26 +    if pgip_parser a = b then ()
    4.27      else error("PGIP test: expected two parses to be equal, for input:\n" ^ a)
    4.28  
    4.29  in
     5.1 --- a/src/Pure/ProofGeneral/pgip_types.ML	Fri Dec 29 18:25:45 2006 +0100
     5.2 +++ b/src/Pure/ProofGeneral/pgip_types.ML	Fri Dec 29 18:25:46 2006 +0100
     5.3 @@ -2,7 +2,7 @@
     5.4      ID:         $Id$
     5.5      Author:     David Aspinall
     5.6  
     5.7 -PGIP abstraction: types and conversions
     5.8 +PGIP abstraction: types and conversions.
     5.9  *)
    5.10  
    5.11  (* TODO: PGML *)
    5.12 @@ -152,7 +152,7 @@
    5.13        | ObjType    => "type"
    5.14        | ObjOther s => s
    5.15  
    5.16 -val attrs_of_objtype = (attr "objtype") o name_of_objtype
    5.17 +val attrs_of_objtype = attr "objtype" o name_of_objtype
    5.18  
    5.19  fun objtype_of_attrs attrs = case get_attr "objtype" attrs of
    5.20         "file" => ObjFile
    5.21 @@ -289,7 +289,7 @@
    5.22  	XML.Elem (elt, (desc_attr @ attrs), (map pgipdtype_to_xml typargs))
    5.23      end
    5.24  
    5.25 -val pgiptype_to_xml = pgipdtype_to_xml o (pair NONE)
    5.26 +val pgiptype_to_xml = pgipdtype_to_xml o pair NONE
    5.27  
    5.28  fun read_pguval Pgipnull s = 
    5.29      if s="" then Pgvalnull
    5.30 @@ -306,7 +306,7 @@
    5.31    | read_pguval (Pgipchoice tydescs) s = 
    5.32      let 
    5.33  	(* Union type: match first in list *)
    5.34 -	fun getty (Pgipdtype(_,ty)) = ty
    5.35 +	fun getty (Pgipdtype(_, ty)) = ty
    5.36  	val uval = get_first 
    5.37  		       (fn ty => SOME (read_pguval ty s) handle PGIP _ => NONE)
    5.38  		       (map getty tydescs)
    5.39 @@ -318,11 +318,11 @@
    5.40  fun read_pgval ty s = (ty, read_pguval ty s)
    5.41  	    
    5.42  fun pgval_to_string (_, Pgvalnull) = ""
    5.43 -  | pgval_to_string (_,(Pgvalbool b)) = bool_to_pgstring b
    5.44 -  | pgval_to_string (_,(Pgvalnat n))  = int_to_pgstring n
    5.45 -  | pgval_to_string (_,(Pgvalint i))  = int_to_pgstring i
    5.46 -  | pgval_to_string (_,(Pgvalconst c)) = string_to_pgstring c
    5.47 -  | pgval_to_string (_,(Pgvalstring s)) = string_to_pgstring s
    5.48 +  | pgval_to_string (_, Pgvalbool b) = bool_to_pgstring b
    5.49 +  | pgval_to_string (_, Pgvalnat n) = int_to_pgstring n
    5.50 +  | pgval_to_string (_, Pgvalint i) = int_to_pgstring i
    5.51 +  | pgval_to_string (_, Pgvalconst c) = string_to_pgstring c
    5.52 +  | pgval_to_string (_, Pgvalstring s) = string_to_pgstring s
    5.53  
    5.54  
    5.55  type pgipurl = Path.T    (* URLs: only local files *)
    5.56 @@ -356,7 +356,7 @@
    5.57  fun attrs_of_pgipurl purl = 
    5.58      [("url", "file:" ^ (XML.text (File.platform_path (File.full_path purl))))]
    5.59  
    5.60 -val pgipurl_of_attrs = pgipurl_of_string o (get_attr "url")
    5.61 +val pgipurl_of_attrs = pgipurl_of_string o get_attr "url"
    5.62  
    5.63  fun pgipurl_of_url (Url.File p) = p
    5.64    | pgipurl_of_url url = raise PGIP ("Cannot access non-local/non-file URL " ^ (Url.implode url))
    5.65 @@ -392,8 +392,8 @@
    5.66  
    5.67    fun attrs_of_location ({ descr, url, line, column, char }:location) =
    5.68        let 
    5.69 -	  val descr = opt_attr  "descr"descr
    5.70 -	  val url = the_default [] (Option.map attrs_of_pgipurl url)
    5.71 +	  val descr = opt_attr "descr" descr
    5.72 +	  val url = these (Option.map attrs_of_pgipurl url)
    5.73  	  val line = opt_attr_map int_to_pgstring "line" line
    5.74  	  val column = opt_attr_map int_to_pgstring "column"  column
    5.75  	  val char = opt_attr_map int_to_pgstring "char" char
     6.1 --- a/src/Pure/ProofGeneral/preferences.ML	Fri Dec 29 18:25:45 2006 +0100
     6.2 +++ b/src/Pure/ProofGeneral/preferences.ML	Fri Dec 29 18:25:46 2006 +0100
     6.3 @@ -52,7 +52,7 @@
     6.4  val proof_pref =
     6.5      let 
     6.6  	fun get () = PgipTypes.bool_to_pgstring (! proofs >= 2)
     6.7 -	fun set s = proofs := (if (PgipTypes.read_pgipbool s) then 1 else 2) 
     6.8 +	fun set s = proofs := (if PgipTypes.read_pgipbool s then 1 else 2)
     6.9      in
    6.10  	mkpref get set PgipTypes.Pgipbool "full-proofs" 
    6.11  	       "Record full proof objects internally"
    6.12 @@ -61,7 +61,7 @@
    6.13  val thm_deps_pref = 
    6.14      let 
    6.15  	fun get () = PgipTypes.bool_to_pgstring (Output.has_mode thm_depsN)
    6.16 -	fun set s = if (PgipTypes.read_pgipbool s) then 
    6.17 +	fun set s = if PgipTypes.read_pgipbool s then 
    6.18  			change print_mode (insert (op =) thm_depsN)
    6.19  		    else 
    6.20  			change print_mode (remove (op =) thm_depsN) 
    6.21 @@ -143,7 +143,7 @@
    6.22  	       "Take a few short cuts",
    6.23       bool_pref Toplevel.skip_proofs
    6.24  	       "skip-proofs"
    6.25 -	       "Ignore proof scripts (interactive-only)"]
    6.26 +	       "Skip over proofs (interactive-only)"]
    6.27  
    6.28  val preferences = 
    6.29      [("Display", display_preferences),
     7.1 --- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Fri Dec 29 18:25:45 2006 +0100
     7.2 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Fri Dec 29 18:25:46 2006 +0100
     7.3 @@ -9,7 +9,7 @@
     7.4  signature PROOF_GENERAL =
     7.5  sig
     7.6    val init: bool -> unit
     7.7 -  val init_pgip: bool -> unit	        (* for compatibility; always fails *)
     7.8 +  val init_pgip: bool -> unit           (* for compatibility; always fails *)
     7.9    val write_keywords: string -> unit
    7.10  end;
    7.11  
    7.12 @@ -22,7 +22,6 @@
    7.13  
    7.14  val proof_generalN = "ProofGeneralEmacs";  (*token markup (colouring vars, etc.)*)
    7.15  val pgasciiN = "PGASCII";                  (*plain 7-bit ASCII communication*)
    7.16 -val xsymbolsN = Symbol.xsymbolsN;          (*X-Symbol symbols*)
    7.17  val thm_depsN = "thm_deps";                (*meta-information about theorem deps*)
    7.18  
    7.19  fun special oct =
    7.20 @@ -38,7 +37,7 @@
    7.21    | xsym_output s = if Symbol.is_raw s then Symbol.decode_raw s else s;
    7.22  
    7.23  fun xsymbols_output s =
    7.24 -  if Output.has_mode xsymbolsN andalso exists_string (equal "\\") s then
    7.25 +  if Output.has_mode Symbol.xsymbolsN andalso exists_string (equal "\\") s then
    7.26      let val syms = Symbol.explode s
    7.27      in (implode (map xsym_output syms), real (Symbol.length syms)) end
    7.28    else Symbol.default_output s;
    7.29 @@ -46,7 +45,7 @@
    7.30  in
    7.31  
    7.32  fun setup_xsymbols_output () =
    7.33 -  Output.add_mode xsymbolsN
    7.34 +  Output.add_mode Symbol.xsymbolsN
    7.35      (xsymbols_output, K xsymbols_output, Symbol.default_indent, Symbol.encode_raw);
    7.36  
    7.37  end;
    7.38 @@ -119,18 +118,16 @@
    7.39  fun emacs_notify s = decorate (special "360") (special "361") "" s;
    7.40  
    7.41  fun tell_clear_goals () =
    7.42 -    emacs_notify "Proof General, please clear the goals buffer.";
    7.43 +  emacs_notify "Proof General, please clear the goals buffer.";
    7.44  
    7.45  fun tell_clear_response () =
    7.46 -    emacs_notify "Proof General, please clear the response buffer.";
    7.47 +  emacs_notify "Proof General, please clear the response buffer.";
    7.48  
    7.49  fun tell_file_loaded path =
    7.50 -    emacs_notify ("Proof General, this file is loaded: " ^ 
    7.51 -		  quote (File.platform_path path));
    7.52 +  emacs_notify ("Proof General, this file is loaded: " ^ quote (File.platform_path path));
    7.53  
    7.54  fun tell_file_retracted path =
    7.55 -    emacs_notify ("Proof General, you can unlock the file " 
    7.56 -		  ^ quote (File.platform_path path));
    7.57 +  emacs_notify ("Proof General, you can unlock the file " ^ quote (File.platform_path path));
    7.58  
    7.59  
    7.60  (* theory / proof state output *)
    7.61 @@ -221,11 +218,11 @@
    7.62  val welcome = priority o Session.welcome;
    7.63  
    7.64  fun restart () =
    7.65 -    (sync_thy_loader ();
    7.66 -     tell_clear_goals ();
    7.67 -     tell_clear_response ();
    7.68 -     welcome ();
    7.69 -     raise Toplevel.RESTART)
    7.70 + (sync_thy_loader ();
    7.71 +  tell_clear_goals ();
    7.72 +  tell_clear_response ();
    7.73 +  welcome ();
    7.74 +  raise Toplevel.RESTART);
    7.75  
    7.76  
    7.77  (* theorem dependency output *)
    7.78 @@ -316,27 +313,25 @@
    7.79  
    7.80  fun set_prompts () = ml_prompts "ML> " "ML# "
    7.81  
    7.82 -fun init_setup () =
    7.83 -  (conditional (not (! initialized)) (fn () =>
    7.84 -   (setmp warning_fn (K ()) init_outer_syntax ();
    7.85 -    setup_xsymbols_output ();
    7.86 -    setup_messages ();
    7.87 -    ProofGeneralPgip.init_pgip_channel (!priority_fn);
    7.88 -    setup_state ();
    7.89 -    setup_thy_loader ();
    7.90 -    setup_present_hook ();
    7.91 -    set initialized; ()));
    7.92 -  sync_thy_loader ();
    7.93 -  change print_mode (cons proof_generalN o remove (op =) proof_generalN);
    7.94 -  set_prompts ())
    7.95 -
    7.96 -fun init true = (init_setup ();
    7.97 -		 Isar.sync_main ())
    7.98 -  | init false = Output.panic "Interface support no longer available for Isabelle/classic mode."
    7.99 +fun init false =
   7.100 +      Output.panic "Interface support no longer available for Isabelle/classic mode."
   7.101 +  | init true =
   7.102 +      (conditional (not (! initialized)) (fn () =>
   7.103 +       (setmp warning_fn (K ()) init_outer_syntax ();
   7.104 +        setup_xsymbols_output ();
   7.105 +        setup_messages ();
   7.106 +        ProofGeneralPgip.init_pgip_channel (! priority_fn);
   7.107 +        setup_state ();
   7.108 +        setup_thy_loader ();
   7.109 +        setup_present_hook ();
   7.110 +        set initialized; ()));
   7.111 +      sync_thy_loader ();
   7.112 +      change print_mode (cons proof_generalN o remove (op =) proof_generalN);
   7.113 +      set_prompts ();
   7.114 +      Isar.sync_main ());
   7.115  
   7.116  fun init_pgip false = init true
   7.117 -  | init_pgip true = Output.panic "No PGIP here, please use ProofGeneralPgip.init_pgip (update your isabelle-process script)."
   7.118 -
   7.119 +  | init_pgip true = Output.panic "No PGIP here, please use ProofGeneralPgip.init_pgip."
   7.120  
   7.121  
   7.122  
   7.123 @@ -345,8 +340,7 @@
   7.124  local
   7.125  
   7.126  val regexp_meta = member (op =) (explode ".*+?[]^$");
   7.127 -val regexp_quote =
   7.128 -  implode o map (fn c => if regexp_meta c then "\\\\" ^ c else c) o explode;
   7.129 +val regexp_quote = translate_string (fn c => if regexp_meta c then "\\\\" ^ c else c);
   7.130  
   7.131  fun defconst name strs =
   7.132    "\n(defconst isar-keywords-" ^ name ^
   7.133 @@ -363,7 +357,7 @@
   7.134    \;; $" ^ "Id$\n\
   7.135    \;;\n" ^
   7.136    defconst "major" (map #1 commands) ^
   7.137 -  defconst "minor" (List.filter Syntax.is_identifier keywords) ^
   7.138 +  defconst "minor" (filter Syntax.is_identifier keywords) ^
   7.139    implode (map (make_elisp_commands commands) OuterKeyword.kinds) ^
   7.140    "\n(provide 'isar-keywords)\n";
   7.141  
   7.142 @@ -376,5 +370,4 @@
   7.143  
   7.144  end;
   7.145  
   7.146 -
   7.147  end;
     8.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Fri Dec 29 18:25:45 2006 +0100
     8.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Fri Dec 29 18:25:46 2006 +0100
     8.3 @@ -3,17 +3,17 @@
     8.4      Author:     David Aspinall and Markus Wenzel
     8.5  
     8.6  Isabelle configuration for Proof General using PGIP protocol.
     8.7 -See http://proofgeneral.inf.ed.ac.uk/kit  
     8.8 +See http://proofgeneral.inf.ed.ac.uk/kit
     8.9  *)
    8.10  
    8.11  
    8.12  signature PROOF_GENERAL_PGIP =
    8.13  sig
    8.14 -  val init_pgip: bool -> unit		  (* main PGIP loop with true; fail with false *)
    8.15 +  val init_pgip: bool -> unit             (* main PGIP loop with true; fail with false *)
    8.16  
    8.17    (* These two are just to support the semi-PGIP Emacs mode *)
    8.18 -  val init_pgip_channel: (string -> unit) -> unit 
    8.19 -  val process_pgip: string -> unit     
    8.20 +  val init_pgip_channel: (string -> unit) -> unit
    8.21 +  val process_pgip: string -> unit
    8.22  end
    8.23  
    8.24  structure ProofGeneralPgip : PROOF_GENERAL_PGIP  =
    8.25 @@ -26,7 +26,6 @@
    8.26  (* print modes *)
    8.27  
    8.28  val proof_generalN = "ProofGeneral";  (*token markup (colouring vars, etc.)*)
    8.29 -val xsymbolsN = Symbol.xsymbolsN;     (*X-Symbol symbols*)
    8.30  val pgmlN = "PGML";                   (*XML escapes and PGML symbol elements*)
    8.31  val pgmlatomsN = "PGMLatoms";         (*variable kind decorations*)
    8.32  val thm_depsN = "thm_deps";           (*meta-information about theorem deps*)
    8.33 @@ -40,7 +39,7 @@
    8.34    | xsym_output s = if Symbol.is_raw s then Symbol.decode_raw s else s;
    8.35  
    8.36  fun xsymbols_output s =
    8.37 -  if Output.has_mode xsymbolsN andalso exists_string (equal "\\") s then
    8.38 +  if Output.has_mode Symbol.xsymbolsN andalso exists_string (equal "\\") s then
    8.39      let val syms = Symbol.explode s
    8.40      in (implode (map xsym_output syms), real (Symbol.length syms)) end
    8.41    else Symbol.default_output s;
    8.42 @@ -49,7 +48,7 @@
    8.43  fun pgml_sym s =
    8.44    (case Symbol.decode s of
    8.45      Symbol.Char s => XML.text s
    8.46 -  | Symbol.Sym sn => XML.element "sym" [("name", sn)] [XML.text s] 
    8.47 +  | Symbol.Sym sn => XML.element "sym" [("name", sn)] [XML.text s]
    8.48    | Symbol.Ctrl sn => XML.element "ctrl" [("name", sn)] [XML.text s] (* FIXME: no such PGML! *)
    8.49    | Symbol.Raw s => s);
    8.50  
    8.51 @@ -60,7 +59,7 @@
    8.52  in
    8.53  
    8.54  fun setup_xsymbols_output () =
    8.55 -  Output.add_mode xsymbolsN
    8.56 +  Output.add_mode Symbol.xsymbolsN
    8.57      (xsymbols_output, K xsymbols_output, Symbol.default_indent, Symbol.encode_raw);
    8.58  
    8.59  fun setup_pgml_output () =
    8.60 @@ -84,7 +83,7 @@
    8.61  
    8.62  fun xml_atom kind x = XML.element "atom" [("kind", kind)] [XML.text x];
    8.63  
    8.64 -fun tagit kind x = 
    8.65 +fun tagit kind x =
    8.66   (xml_atom kind x, real (Symbol.length (Symbol.explode x)));
    8.67  
    8.68  fun free_or_skolem x =
    8.69 @@ -130,15 +129,15 @@
    8.70    fun pgip_serial () = inc pgip_seq
    8.71  
    8.72    fun assemble_pgips pgips =
    8.73 -    Pgip { tag = SOME pgip_tag, 
    8.74 -	   class = pgip_class,
    8.75 -	   seq = pgip_serial(),
    8.76 -	   id = !pgip_id,
    8.77 -	   destid = !pgip_refid,
    8.78 -	   (* destid=refid since Isabelle only communicates back to sender *)
    8.79 -	   refid  = !pgip_refid,
    8.80 -	   refseq = !pgip_refseq,
    8.81 -	   content = pgips }
    8.82 +    Pgip { tag = SOME pgip_tag,
    8.83 +           class = pgip_class,
    8.84 +           seq = pgip_serial(),
    8.85 +           id = !pgip_id,
    8.86 +           destid = !pgip_refid,
    8.87 +           (* destid=refid since Isabelle only communicates back to sender *)
    8.88 +           refid  = !pgip_refid,
    8.89 +           refseq = !pgip_refseq,
    8.90 +           content = pgips }
    8.91  in
    8.92  
    8.93  fun init_pgip_session_id () =
    8.94 @@ -147,10 +146,10 @@
    8.95  
    8.96  fun matching_pgip_id id = (id = !pgip_id)
    8.97  
    8.98 -val output_xml_fn = ref writeln_default  
    8.99 +val output_xml_fn = ref writeln_default
   8.100  fun output_xml s = (!output_xml_fn) (XML.string_of_tree s);  (* TODO: string buffer *)
   8.101  
   8.102 -fun issue_pgip_rawtext str = 
   8.103 +fun issue_pgip_rawtext str =
   8.104      output_xml (PgipOutput.output (assemble_pgips [XML.Rawtext str]))
   8.105  
   8.106  fun issue_pgips pgipops =
   8.107 @@ -169,29 +168,29 @@
   8.108      val delayed_msgs = ref []
   8.109  
   8.110      fun queue_or_issue pgip =
   8.111 -	if (! delay_msgs) then
   8.112 -	    delayed_msgs := pgip :: ! delayed_msgs
   8.113 -	else issue_pgip pgip
   8.114 +        if ! delay_msgs then
   8.115 +            delayed_msgs := pgip :: ! delayed_msgs
   8.116 +        else issue_pgip pgip
   8.117  in
   8.118 -    fun normalmsg area cat urgent s = 
   8.119 -	let 
   8.120 -	    val content = XML.Elem("pgmltext",[],[XML.Rawtext s])
   8.121 -	    val pgip = Normalresponse {area=area,messagecategory=cat,
   8.122 -				       urgent=urgent,content=[content] }
   8.123 -	in
   8.124 -	    queue_or_issue pgip
   8.125 -	end
   8.126 +    fun normalmsg area cat urgent s =
   8.127 +        let
   8.128 +            val content = XML.Elem("pgmltext",[],[XML.Rawtext s])
   8.129 +            val pgip = Normalresponse {area=area,messagecategory=cat,
   8.130 +                                       urgent=urgent,content=[content] }
   8.131 +        in
   8.132 +            queue_or_issue pgip
   8.133 +        end
   8.134  
   8.135      fun errormsg fatality s =
   8.136 -	let
   8.137 +        let
   8.138                val content = XML.Elem("pgmltext",[],[XML.Rawtext s])
   8.139 -	      val pgip = Errorresponse {area=NONE,fatality=fatality,
   8.140 -					content=[content], 
   8.141 -					(* FIXME: pass in locations *)
   8.142 -					location=NONE}
   8.143 -	in 
   8.144 -	    queue_or_issue pgip
   8.145 -	end
   8.146 +              val pgip = Errorresponse {area=NONE,fatality=fatality,
   8.147 +                                        content=[content],
   8.148 +                                        (* FIXME: pass in locations *)
   8.149 +                                        location=NONE}
   8.150 +        in
   8.151 +            queue_or_issue pgip
   8.152 +        end
   8.153  
   8.154      fun start_delay_msgs () = (set delay_msgs; delayed_msgs := [])
   8.155      fun end_delayed_msgs () = (reset delay_msgs; ! delayed_msgs)
   8.156 @@ -199,7 +198,7 @@
   8.157  
   8.158  (* NB: all of the standard error/message functions now expect already-escaped text.
   8.159     FIXME: this may cause us problems now we're generating trees; on the other
   8.160 -   hand the output functions were tuned some time ago, so it ought to be 
   8.161 +   hand the output functions were tuned some time ago, so it ought to be
   8.162     enough to use Rawtext always above. *)
   8.163  
   8.164  fun setup_messages () =
   8.165 @@ -227,10 +226,10 @@
   8.166  
   8.167  fun statedisplay prts =
   8.168      let
   8.169 -	val display = Pretty.output (Pretty.chunks prts)
   8.170 -	val statedisplay = XML.Elem("statedisplay",[], [XML.Rawtext display])
   8.171 +        val display = Pretty.output (Pretty.chunks prts)
   8.172 +        val statedisplay = XML.Elem("statedisplay",[], [XML.Rawtext display])
   8.173      in
   8.174 -	issue_pgip (Proofstate {pgml=[XML.Elem("pgml",[],[statedisplay])]})
   8.175 +        issue_pgip (Proofstate {pgml=[XML.Elem("pgml",[],[statedisplay])]})
   8.176      end
   8.177  
   8.178  fun print_current_goals n m st =
   8.179 @@ -245,7 +244,7 @@
   8.180    (Display.print_current_goals_fn := print_current_goals;
   8.181     Toplevel.print_state_fn := print_state);
   8.182        (*    Toplevel.prompt_state_fn := (fn s => suffix (special "372")
   8.183 -					(Toplevel.prompt_state_default s))); *)
   8.184 +                                        (Toplevel.prompt_state_default s))); *)
   8.185  
   8.186  end;
   8.187  
   8.188 @@ -327,12 +326,12 @@
   8.189  val spaces_quote = space_implode " " o map quote;
   8.190  
   8.191  fun thm_deps_message (thms, deps) =
   8.192 -    let 
   8.193 -	val valuethms = XML.Elem("value",[("name", "thms")],[XML.Text thms])
   8.194 -	val valuedeps = XML.Elem("value",[("name", "deps")],[XML.Text deps])
   8.195 +    let
   8.196 +        val valuethms = XML.Elem("value",[("name", "thms")],[XML.Text thms])
   8.197 +        val valuedeps = XML.Elem("value",[("name", "deps")],[XML.Text deps])
   8.198      in
   8.199 -	issue_pgip (Metainforesponse {attrs=[("infotype", "isabelle_theorem_dependencies")],
   8.200 -				      content=[valuethms,valuedeps]})
   8.201 +        issue_pgip (Metainforesponse {attrs=[("infotype", "isabelle_theorem_dependencies")],
   8.202 +                                      content=[valuethms,valuedeps]})
   8.203      end
   8.204  
   8.205  (* FIXME: check this uses non-transitive closure function here *)
   8.206 @@ -356,14 +355,14 @@
   8.207  
   8.208  (** lexicalstructure element with keywords (PGIP version of elisp keywords file) **)
   8.209  
   8.210 -fun lexicalstructure_keywords () = 
   8.211 +fun lexicalstructure_keywords () =
   8.212      let val commands = OuterSyntax.dest_keywords ()
   8.213 -	fun category_of k = if (k mem commands) then "major" else "minor"
   8.214 +        fun category_of k = if k mem commands then "major" else "minor"
   8.215           (* NB: we might filter to only include words like elisp case (OuterSyntax.is_keyword). *)
   8.216 -    	fun keyword_elt (keyword,help,kind,_) = 
   8.217 -  	    XML.Elem("keyword", [("word", keyword), ("category", category_of kind)],
   8.218 -	  	     [XML.Elem("shorthelp", [], [XML.Text help])])
   8.219 -        in 	    	    
   8.220 +        fun keyword_elt (keyword,help,kind,_) =
   8.221 +            XML.Elem("keyword", [("word", keyword), ("category", category_of kind)],
   8.222 +                     [XML.Elem("shorthelp", [], [XML.Text help])])
   8.223 +        in
   8.224              (* Also, note we don't call init_outer_syntax here to add interface commands,
   8.225              but they should never appear in scripts anyway so it shouldn't matter *)
   8.226              Lexicalstructure {content = map keyword_elt (OuterSyntax.dest_parsers()) }
   8.227 @@ -378,34 +377,34 @@
   8.228  local
   8.229      val isabellewww = "http://isabelle.in.tum.de/"
   8.230      val staticconfig = "~~/lib/ProofGeneral/pgip_isar.xml"
   8.231 -    fun orenv v d = case (getenv v) of "" => d  | s => s
   8.232 +    fun orenv v d = case getenv v of "" => d  | s => s
   8.233      fun config_file()  = orenv "ISABELLE_PGIPCONFIG" staticconfig
   8.234      fun isabelle_www() = orenv "ISABELLE_HOMEPAGE" isabellewww
   8.235  in
   8.236  fun send_pgip_config () =
   8.237      let
   8.238          val path = Path.explode (config_file())
   8.239 -        val exists = File.exists path
   8.240 +        val ex = File.exists path
   8.241  
   8.242 -	val wwwpage = 
   8.243 -	    (Url.explode (isabelle_www()))
   8.244 -	    handle _ => 
   8.245 -		   (Output.panic 
   8.246 -			("Error in URL in environment variable ISABELLE_HOMEPAGE.");
   8.247 -			Url.explode isabellewww)
   8.248 -		     
   8.249 -	val proverinfo =
   8.250 +        val wwwpage =
   8.251 +            (Url.explode (isabelle_www()))
   8.252 +            handle _ =>
   8.253 +                   (Output.panic
   8.254 +                        ("Error in URL in environment variable ISABELLE_HOMEPAGE.");
   8.255 +                        Url.explode isabellewww)
   8.256 +
   8.257 +        val proverinfo =
   8.258              Proverinfo { name = "Isabelle",
   8.259 -			 version = version,
   8.260 -			 instance = Session.name(), 
   8.261 -			 descr = "The Isabelle/Isar theorem prover",
   8.262 -			 url = wwwpage,
   8.263 -			 filenameextns = ".thy;" }
   8.264 +                         version = version,
   8.265 +                         instance = Session.name(),
   8.266 +                         descr = "The Isabelle/Isar theorem prover",
   8.267 +                         url = wwwpage,
   8.268 +                         filenameextns = ".thy;" }
   8.269      in
   8.270 -        if exists then
   8.271 -            (issue_pgip proverinfo; 
   8.272 -	     issue_pgip_rawtext (File.read path);
   8.273 -	     issue_pgip (lexicalstructure_keywords()))
   8.274 +        if ex then
   8.275 +            (issue_pgip proverinfo;
   8.276 +             issue_pgip_rawtext (File.read path);
   8.277 +             issue_pgip (lexicalstructure_keywords()))
   8.278          else Output.panic ("PGIP configuration file \"" ^ config_file() ^ "\" not found")
   8.279      end;
   8.280  end
   8.281 @@ -421,7 +420,7 @@
   8.282        |> map #3
   8.283        |> Toplevel.>>>;
   8.284  
   8.285 -(* TODO: 
   8.286 +(* TODO:
   8.287      - apply a command given a transition function, e.g. IsarCmd.undo.
   8.288      - fix position from path of currently open file [line numbers risk garbling though].
   8.289  *)
   8.290 @@ -433,8 +432,8 @@
   8.291          val (path,extn) = Path.split_ext (Path.explode file)
   8.292      in
   8.293          case extn of
   8.294 -            "" => isarcmd ("use_thy " ^ (quote (Path.implode path)))
   8.295 -          | "thy" => isarcmd ("use_thy " ^ (quote (Path.implode path)))
   8.296 +            "" => isarcmd ("use_thy " ^ quote (Path.implode path))
   8.297 +          | "thy" => isarcmd ("use_thy " ^ quote (Path.implode path))
   8.298            | "ML" => isarcmd ("use " ^ quote file)
   8.299            | other => error ("Don't know how to read a file with extension " ^ other)
   8.300      end
   8.301 @@ -443,54 +442,54 @@
   8.302  (******* PGIP actions *******)
   8.303  
   8.304  
   8.305 -(* Responses to each of the PGIP input commands. 
   8.306 +(* Responses to each of the PGIP input commands.
   8.307     These are programmed uniformly for extensibility. *)
   8.308  
   8.309 -fun askpgip (Askpgip vs) = 
   8.310 +fun askpgip (Askpgip vs) =
   8.311      issue_pgip
   8.312          (Usespgip { version = PgipIsabelle.isabelle_pgip_version_supported,
   8.313 -		    pgipelems = PgipIsabelle.accepted_inputs })
   8.314 +                    pgipelems = PgipIsabelle.accepted_inputs })
   8.315  
   8.316 -fun askpgml (Askpgml vs) = 
   8.317 +fun askpgml (Askpgml vs) =
   8.318      issue_pgip
   8.319 -	(Usespgml { version = PgipIsabelle.isabelle_pgml_version_supported })
   8.320 +        (Usespgml { version = PgipIsabelle.isabelle_pgml_version_supported })
   8.321  
   8.322  fun askprefs (Askprefs vs) =
   8.323 -    let 
   8.324 -	fun preference_of {name, descr, default, pgiptype, get, set } = 
   8.325 -	    { name = name, descr = SOME descr, default = SOME default, 
   8.326 -	      pgiptype = pgiptype }
   8.327 +    let
   8.328 +        fun preference_of {name, descr, default, pgiptype, get, set } =
   8.329 +            { name = name, descr = SOME descr, default = SOME default,
   8.330 +              pgiptype = pgiptype }
   8.331      in
   8.332 -	List.app (fn (prefcat, prefs) =>
   8.333 -		     issue_pgip (Hasprefs {prefcategory=SOME prefcat, 
   8.334 -					   prefs=map preference_of prefs}))
   8.335 +        List.app (fn (prefcat, prefs) =>
   8.336 +                     issue_pgip (Hasprefs {prefcategory=SOME prefcat,
   8.337 +                                           prefs=map preference_of prefs}))
   8.338                   Preferences.preferences
   8.339 -    end 
   8.340 +    end
   8.341  
   8.342  fun askconfig (Askconfig vs) = () (* TODO: add config response *)
   8.343  
   8.344  local
   8.345 -    fun lookuppref pref = 
   8.346 -	case AList.lookup (op =) 
   8.347 -			  (map (fn p => (#name p,p))
   8.348 -			       (maps snd Preferences.preferences)) pref of
   8.349 -	    NONE => error ("Unknown prover preference: " ^ quote pref)
   8.350 -	  | SOME p => p
   8.351 +    fun lookuppref pref =
   8.352 +        case AList.lookup (op =)
   8.353 +                          (map (fn p => (#name p,p))
   8.354 +                               (maps snd Preferences.preferences)) pref of
   8.355 +            NONE => error ("Unknown prover preference: " ^ quote pref)
   8.356 +          | SOME p => p
   8.357  in
   8.358 -fun setpref (Setpref vs) = 
   8.359 -    let 
   8.360 -	val name = #name vs
   8.361 -	val value = #value vs
   8.362 -	val set = #set (lookuppref name)
   8.363 +fun setpref (Setpref vs) =
   8.364 +    let
   8.365 +        val name = #name vs
   8.366 +        val value = #value vs
   8.367 +        val set = #set (lookuppref name)
   8.368      in
   8.369 -	set value
   8.370 +        set value
   8.371      end
   8.372  
   8.373  fun getpref (Getpref vs) =
   8.374 -    let 
   8.375 -	val name = #name vs
   8.376 -	val get = #get (lookuppref name)
   8.377 -    in 
   8.378 +    let
   8.379 +        val name = #name vs
   8.380 +        val get = #get (lookuppref name)
   8.381 +    in
   8.382          issue_pgip (Prefval {name=name, value=get ()})
   8.383      end
   8.384  end
   8.385 @@ -503,30 +502,30 @@
   8.386  
   8.387  fun stopquiet vs = isarcmd "enable_pr"
   8.388  
   8.389 -fun pgmlsymbolson vs = 
   8.390 +fun pgmlsymbolson vs =
   8.391      change print_mode (fn mode =>
   8.392 -			  remove (op =) Symbol.xsymbolsN mode @ [Symbol.xsymbolsN])
   8.393 +                          remove (op =) Symbol.xsymbolsN mode @ [Symbol.xsymbolsN])
   8.394  
   8.395  fun pgmlsymbolsoff vs =
   8.396      change print_mode (remove (op =) Symbol.xsymbolsN)
   8.397  
   8.398 -fun dostep (Dostep vs) = 
   8.399 -    let 
   8.400 -	val text = #text vs
   8.401 -    in 
   8.402 -	isarcmd text
   8.403 +fun dostep (Dostep vs) =
   8.404 +    let
   8.405 +        val text = #text vs
   8.406 +    in
   8.407 +        isarcmd text
   8.408      end
   8.409  
   8.410  fun undostep (Undostep vs) =
   8.411 -    let 
   8.412 -	val times = #times vs
   8.413 -    in 
   8.414 -	isarcmd ("undos_proof " ^ (Int.toString times))
   8.415 +    let
   8.416 +        val times = #times vs
   8.417 +    in
   8.418 +        isarcmd ("undos_proof " ^ Int.toString times)
   8.419      end
   8.420  
   8.421  fun redostep vs = isarcmd "redo"
   8.422 -    
   8.423 -fun abortgoal vs = isarcmd "ProofGeneral.kill_proof" 
   8.424 +
   8.425 +fun abortgoal vs = isarcmd "ProofGeneral.kill_proof"
   8.426  
   8.427  
   8.428  (*** PGIP identifier tables ***)
   8.429 @@ -536,126 +535,126 @@
   8.430  fun delids t = issue_pgip (Delids {idtables = [t]})
   8.431  
   8.432  (*
   8.433 - fun delallids ty = 
   8.434 -     issue_pgip (Setids {idtables = 
   8.435 -	 		[{context=NONE,objtype=ty,ids=[]}]}) *)
   8.436 + fun delallids ty =
   8.437 +     issue_pgip (Setids {idtables =
   8.438 +                        [{context=NONE,objtype=ty,ids=[]}]}) *)
   8.439  
   8.440 -fun askids (Askids vs) = 
   8.441 +fun askids (Askids vs) =
   8.442      let
   8.443 -	val url = #url vs	     (* ask for identifiers within a file *)
   8.444 -	val thyname = #thyname vs    (* ask for identifiers within a theory *)
   8.445 -	val objtype = #objtype vs    (* ask for identifiers of a particular type *)
   8.446 +        val url = #url vs            (* ask for identifiers within a file *)
   8.447 +        val thyname = #thyname vs    (* ask for identifiers within a theory *)
   8.448 +        val objtype = #objtype vs    (* ask for identifiers of a particular type *)
   8.449  
   8.450 -	fun idtable ty ctx ids = {objtype=ty,context=ctx,ids=ids}
   8.451 +        fun idtable ty ctx ids = {objtype=ty,context=ctx,ids=ids}
   8.452  
   8.453 -	val thms_of_thy = (map fst) o PureThy.thms_of o ThyInfo.get_theory
   8.454 -    in 
   8.455 -(*	case (url_attr,thyname,objtype) of
   8.456 -	    (NONE,NONE,NONE) => 
   8.457 -*)	    (* top-level: return *)
   8.458 +        val thms_of_thy = map fst o PureThy.thms_of o ThyInfo.get_theory
   8.459 +    in
   8.460 +(*      case (url_attr,thyname,objtype) of
   8.461 +            (NONE,NONE,NONE) =>
   8.462 +*)          (* top-level: return *)
   8.463  
   8.464 -	(* TODO: add askids for "file" here, which returns single theory with same name *)
   8.465 +        (* TODO: add askids for "file" here, which returns single theory with same name *)
   8.466          (* FIXME: objtypes on both sides *)
   8.467 -	case (thyname,objtype) of 
   8.468 +        case (thyname,objtype) of
   8.469             (* only files known in top context *)
   8.470 -	   (NONE, NONE)		      => setids (idtable ObjFile NONE (ThyInfo.names())) (*FIXME: uris?*)
   8.471 -	 | (NONE, SOME ObjFile)        => setids (idtable ObjFile NONE (ThyInfo.names())) (* ditto *)
   8.472 -	 | (SOME fi, SOME ObjFile)     => setids (idtable ObjTheory (SOME fi) [fi]) (* FIXME: lookup file *)
   8.473 -	 | (NONE, SOME ObjTheory)      => setids (idtable ObjTheory NONE (ThyInfo.names()))
   8.474 -	 | (SOME thy, SOME ObjTheory)  => setids (idtable ObjTheory (SOME thy) (ThyInfo.get_preds thy))
   8.475 -	 | (SOME thy, SOME ObjTheorem) => setids (idtable ObjTheorem (SOME thy) (thms_of_thy thy))
   8.476 -         (* next case is both of above.  FIXME: cleanup this *)					 
   8.477 -	 | (SOME thy, NONE) => (setids (idtable ObjTheory (SOME thy) (ThyInfo.get_preds thy));
   8.478 -				setids (idtable ObjTheorem (SOME thy) (thms_of_thy thy)))
   8.479 -	 | (_, SOME ot) => error ("No objects of type "^(PgipTypes.name_of_objtype ot)^" are available here.")
   8.480 +           (NONE, NONE)               => setids (idtable ObjFile NONE (ThyInfo.names())) (*FIXME: uris?*)
   8.481 +         | (NONE, SOME ObjFile)        => setids (idtable ObjFile NONE (ThyInfo.names())) (* ditto *)
   8.482 +         | (SOME fi, SOME ObjFile)     => setids (idtable ObjTheory (SOME fi) [fi]) (* FIXME: lookup file *)
   8.483 +         | (NONE, SOME ObjTheory)      => setids (idtable ObjTheory NONE (ThyInfo.names()))
   8.484 +         | (SOME thy, SOME ObjTheory)  => setids (idtable ObjTheory (SOME thy) (ThyInfo.get_preds thy))
   8.485 +         | (SOME thy, SOME ObjTheorem) => setids (idtable ObjTheorem (SOME thy) (thms_of_thy thy))
   8.486 +         (* next case is both of above.  FIXME: cleanup this *)
   8.487 +         | (SOME thy, NONE) => (setids (idtable ObjTheory (SOME thy) (ThyInfo.get_preds thy));
   8.488 +                                setids (idtable ObjTheorem (SOME thy) (thms_of_thy thy)))
   8.489 +         | (_, SOME ot) => error ("No objects of type "^(PgipTypes.name_of_objtype ot)^" are available here.")
   8.490      end
   8.491  
   8.492  local
   8.493    (* accumulate printed output in a single PGIP response (inside <pgmltext>) *)
   8.494    fun with_displaywrap pgipfn dispfn =
   8.495        let
   8.496 -	  val lines = ref ([]: string list);
   8.497 -	  fun wlgrablines s = lines := s :: ! lines;
   8.498 +          val lines = ref ([]: string list);
   8.499 +          fun wlgrablines s = lines := s :: ! lines;
   8.500        in
   8.501 -	  setmp writeln_fn wlgrablines dispfn ();
   8.502 -	  issue_pgip (pgipfn (!lines))
   8.503 +          setmp writeln_fn wlgrablines dispfn ();
   8.504 +          issue_pgip (pgipfn (!lines))
   8.505        end;
   8.506  in
   8.507 -fun showid (Showid vs) = 
   8.508 +fun showid (Showid vs) =
   8.509      let
   8.510 -	val thyname = #thyname vs
   8.511 -	val objtype = #objtype vs
   8.512 -	val name = #name vs
   8.513 -	val topthy = Toplevel.theory_of o Toplevel.get_state
   8.514 +        val thyname = #thyname vs
   8.515 +        val objtype = #objtype vs
   8.516 +        val name = #name vs
   8.517 +        val topthy = Toplevel.theory_of o Toplevel.get_state
   8.518  
   8.519 -	fun idvalue objtype name strings =
   8.520 -	    Idvalue { name=name, objtype=objtype,
   8.521 -		      text=[XML.Elem("pgmltext",[],map XML.Text strings)] }
   8.522 +        fun idvalue objtype name strings =
   8.523 +            Idvalue { name=name, objtype=objtype,
   8.524 +                      text=[XML.Elem("pgmltext",[],map XML.Text strings)] }
   8.525  
   8.526 -	fun pthm thy name = print_thm (get_thm thy (Name name))
   8.527 -    in 
   8.528 -	case (thyname, objtype) of 
   8.529 -	    (_,ObjTheory) =>
   8.530 -	    with_displaywrap (idvalue ObjTheory name) 
   8.531 -			     (fn ()=>(print_theory (ThyInfo.get_theory name)))
   8.532 -	  | (SOME thy, ObjTheorem) =>
   8.533 -	    with_displaywrap (idvalue ObjTheorem name) 
   8.534 -			     (fn ()=>(pthm (ThyInfo.get_theory thy) name))
   8.535 -	  | (NONE, ObjTheorem) =>
   8.536 -	    with_displaywrap (idvalue ObjTheorem name) 
   8.537 -			     (fn ()=>pthm (topthy()) name)
   8.538 -	  | (_, ot) => error ("Cannot show objects of type "^(PgipTypes.name_of_objtype ot))
   8.539 +        fun pthm thy name = print_thm (get_thm thy (Name name))
   8.540 +    in
   8.541 +        case (thyname, objtype) of
   8.542 +            (_,ObjTheory) =>
   8.543 +            with_displaywrap (idvalue ObjTheory name)
   8.544 +                             (fn ()=>(print_theory (ThyInfo.get_theory name)))
   8.545 +          | (SOME thy, ObjTheorem) =>
   8.546 +            with_displaywrap (idvalue ObjTheorem name)
   8.547 +                             (fn ()=>(pthm (ThyInfo.get_theory thy) name))
   8.548 +          | (NONE, ObjTheorem) =>
   8.549 +            with_displaywrap (idvalue ObjTheorem name)
   8.550 +                             (fn ()=>pthm (topthy()) name)
   8.551 +          | (_, ot) => error ("Cannot show objects of type "^(PgipTypes.name_of_objtype ot))
   8.552      end
   8.553  
   8.554  (*** Inspecting state ***)
   8.555  
   8.556 -(* The file which is currently being processed interactively.  
   8.557 +(* The file which is currently being processed interactively.
   8.558     In the pre-PGIP code, this was informed to Isabelle and the theory loader
   8.559     on completion, but that allows for circularity in case we read
   8.560     ourselves.  So PGIP opens the filename at the start of a script.
   8.561     We ought to prevent problems by modifying the theory loader to know
   8.562 -   about this special status, but for now we just keep a local reference. 
   8.563 -*) 
   8.564 +   about this special status, but for now we just keep a local reference.
   8.565 +*)
   8.566  
   8.567  val currently_open_file = ref (NONE : pgipurl option)
   8.568  
   8.569 -fun askguise vs = 
   8.570 +fun askguise vs =
   8.571      (* The "guise" is the PGIP abstraction of the prover's state.
   8.572         The <informguise> message is merely used for consistency checking. *)
   8.573 -    let 
   8.574 -	val openfile = !currently_open_file
   8.575 +    let
   8.576 +        val openfile = !currently_open_file
   8.577  
   8.578 -	val topthy = Toplevel.theory_of o Toplevel.get_state
   8.579 -	val topthy_name = Context.theory_name o topthy
   8.580 +        val topthy = Toplevel.theory_of o Toplevel.get_state
   8.581 +        val topthy_name = Context.theory_name o topthy
   8.582  
   8.583 -	val opentheory = SOME (topthy_name()) handle Toplevel.UNDEF => NONE
   8.584 +        val opentheory = SOME (topthy_name()) handle Toplevel.UNDEF => NONE
   8.585  
   8.586 -	fun topproofpos () = try Toplevel.proof_position_of (Isar.state ());
   8.587 -	val openproofpos = topproofpos()
   8.588 +        fun topproofpos () = try Toplevel.proof_position_of (Isar.state ());
   8.589 +        val openproofpos = topproofpos()
   8.590      in
   8.591          issue_pgip (Informguise { file = openfile,
   8.592 -				  theory = opentheory,
   8.593 -				  (* would be nice to get thm name... *)
   8.594 -				  theorem = NONE,
   8.595 -				  proofpos = openproofpos })
   8.596 +                                  theory = opentheory,
   8.597 +                                  (* would be nice to get thm name... *)
   8.598 +                                  theorem = NONE,
   8.599 +                                  proofpos = openproofpos })
   8.600      end
   8.601  
   8.602  fun parsescript (Parsescript vs) =
   8.603      let
   8.604 -	val text = #text vs
   8.605 -	val systemdata = #systemdata vs      
   8.606 -	val location = #location vs   (* TODO: extract position *)
   8.607 +        val text = #text vs
   8.608 +        val systemdata = #systemdata vs
   8.609 +        val location = #location vs   (* TODO: extract position *)
   8.610  
   8.611          val _ = start_delay_msgs ()   (* gather parsing errs/warns *)
   8.612          val doc = PgipParser.pgip_parser text
   8.613          val errs = end_delayed_msgs ()
   8.614  
   8.615 -	val sysattrs = PgipTypes.opt_attr "systemdata" systemdata
   8.616 -	val locattrs = PgipTypes.attrs_of_location location
   8.617 +        val sysattrs = PgipTypes.opt_attr "systemdata" systemdata
   8.618 +        val locattrs = PgipTypes.attrs_of_location location
   8.619       in
   8.620          issue_pgip (Parseresult { attrs= sysattrs@locattrs,
   8.621 -				  doc = doc,
   8.622 -				  errs = (map PgipOutput.output errs) })
   8.623 +                                  doc = doc,
   8.624 +                                  errs = map PgipOutput.output errs })
   8.625      end
   8.626  
   8.627  fun showproofstate vs = isarcmd "pr"
   8.628 @@ -663,33 +662,33 @@
   8.629  fun showctxt vs = isarcmd "print_theory"   (* more useful than print_context *)
   8.630  
   8.631  fun searchtheorems (Searchtheorems vs) =
   8.632 -    let 
   8.633 -	val arg = #arg vs
   8.634 +    let
   8.635 +        val arg = #arg vs
   8.636      in
   8.637 -	isarcmd ("thms_containing " ^ arg)
   8.638 +        isarcmd ("thms_containing " ^ arg)
   8.639      end
   8.640  
   8.641 -fun setlinewidth (Setlinewidth vs) = 
   8.642 -    let 
   8.643 -	val width = #width vs
   8.644 +fun setlinewidth (Setlinewidth vs) =
   8.645 +    let
   8.646 +        val width = #width vs
   8.647      in
   8.648 -	isarcmd ("pretty_setmargin " ^ (Int.toString width)) (* FIXME: conversion back/forth! *)
   8.649 +        isarcmd ("pretty_setmargin " ^ Int.toString width) (* FIXME: conversion back/forth! *)
   8.650      end
   8.651  
   8.652  fun viewdoc (Viewdoc vs) =
   8.653 -    let 
   8.654 -	val arg = #arg vs
   8.655 -    in 
   8.656 -	isarcmd ("print_" ^ arg)   (* FIXME: isatool doc?.  Return URLs, maybe? *)
   8.657 +    let
   8.658 +        val arg = #arg vs
   8.659 +    in
   8.660 +        isarcmd ("print_" ^ arg)   (* FIXME: isatool doc?.  Return URLs, maybe? *)
   8.661      end
   8.662  
   8.663  (*** Theory ***)
   8.664  
   8.665  fun doitem (Doitem vs) =
   8.666      let
   8.667 -	val text = #text vs
   8.668 +        val text = #text vs
   8.669      in
   8.670 -	isarcmd text
   8.671 +        isarcmd text
   8.672      end
   8.673  
   8.674  fun undoitem vs =
   8.675 @@ -698,14 +697,14 @@
   8.676  fun redoitem vs =
   8.677      isarcmd "ProofGeneral.redo"
   8.678  
   8.679 -fun aborttheory vs = 
   8.680 +fun aborttheory vs =
   8.681      isarcmd "init_toplevel"
   8.682  
   8.683  fun retracttheory (Retracttheory vs) =
   8.684 -    let 
   8.685 -	val thyname = #thyname vs
   8.686 +    let
   8.687 +        val thyname = #thyname vs
   8.688      in
   8.689 -	isarcmd ("kill_thy " ^ quote thyname)
   8.690 +        isarcmd ("kill_thy " ^ quote thyname)
   8.691      end
   8.692  
   8.693  
   8.694 @@ -715,16 +714,16 @@
   8.695     their own directory, but when we change directory for a new file we
   8.696     remove the path.  Leaving it there can cause confusion with
   8.697     difference in batch mode.
   8.698 -   NB: PGIP does not assume that the prover has a load path. 
   8.699 +   NB: PGIP does not assume that the prover has a load path.
   8.700  *)
   8.701  
   8.702  local
   8.703      val current_working_dir = ref (NONE : string option)
   8.704  in
   8.705 -fun changecwd_dir newdirpath = 
   8.706 -   let 
   8.707 +fun changecwd_dir newdirpath =
   8.708 +   let
   8.709         val newdir = File.platform_path newdirpath
   8.710 -   in 
   8.711 +   in
   8.712         (case (!current_working_dir) of
   8.713              NONE => ()
   8.714            | SOME dir => ThyLoad.del_path dir;
   8.715 @@ -733,16 +732,16 @@
   8.716     end
   8.717  end
   8.718  
   8.719 -fun changecwd (Changecwd vs) = 
   8.720 -    let 
   8.721 -	val url = #url vs
   8.722 -	val newdir = PgipTypes.path_of_pgipurl url
   8.723 +fun changecwd (Changecwd vs) =
   8.724 +    let
   8.725 +        val url = #url vs
   8.726 +        val newdir = PgipTypes.path_of_pgipurl url
   8.727      in
   8.728 -	changecwd_dir url
   8.729 +        changecwd_dir url
   8.730      end
   8.731  
   8.732  fun openfile (Openfile vs) =
   8.733 -  let 
   8.734 +  let
   8.735        val url = #url vs
   8.736        val filepath = PgipTypes.path_of_pgipurl url
   8.737        val filedir = Path.dir filepath
   8.738 @@ -752,22 +751,22 @@
   8.739        case !currently_open_file of
   8.740            SOME f => raise PGIP ("<openfile> when a file is already open! ")
   8.741          | NONE => (openfile_retract filepath;
   8.742 -		   changecwd_dir filedir;
   8.743 -		   currently_open_file := SOME url)
   8.744 +                   changecwd_dir filedir;
   8.745 +                   currently_open_file := SOME url)
   8.746    end
   8.747  
   8.748  fun closefile vs =
   8.749      case !currently_open_file of
   8.750 -        SOME f => (proper_inform_file_processed (File.platform_path f) 
   8.751 -						(Isar.state());
   8.752 +        SOME f => (proper_inform_file_processed (File.platform_path f)
   8.753 +                                                (Isar.state());
   8.754                     currently_open_file := NONE)
   8.755        | NONE => raise PGIP ("<closefile> when no file is open!")
   8.756  
   8.757 -fun loadfile (Loadfile vs) = 
   8.758 -    let 
   8.759 -	val url = #url vs
   8.760 -    in 
   8.761 -	case !currently_open_file of
   8.762 +fun loadfile (Loadfile vs) =
   8.763 +    let
   8.764 +        val url = #url vs
   8.765 +    in
   8.766 +        case !currently_open_file of
   8.767              SOME f => raise PGIP ("<loadfile> when a file is open!")
   8.768            | NONE => use_thy_or_ml_file (File.platform_path url)
   8.769      end
   8.770 @@ -775,14 +774,14 @@
   8.771  fun abortfile vs =
   8.772      case !currently_open_file of
   8.773          SOME f => (isarcmd "init_toplevel";
   8.774 -		   currently_open_file := NONE)
   8.775 +                   currently_open_file := NONE)
   8.776        | NONE => raise PGIP ("<abortfile> when no file is open!")
   8.777  
   8.778 -fun retractfile (Retractfile vs) = 
   8.779 -    let 
   8.780 -	val url = #url vs
   8.781 +fun retractfile (Retractfile vs) =
   8.782 +    let
   8.783 +        val url = #url vs
   8.784      in
   8.785 -	case !currently_open_file of
   8.786 +        case !currently_open_file of
   8.787              SOME f => raise PGIP ("<retractfile> when a file is open!")
   8.788            | NONE => inform_file_retracted (File.platform_path url)
   8.789      end
   8.790 @@ -791,7 +790,7 @@
   8.791  (*** System ***)
   8.792  
   8.793  fun systemcmd (Systemcmd vs) =
   8.794 -  let 
   8.795 +  let
   8.796        val arg = #arg vs
   8.797    in
   8.798        isarcmd arg
   8.799 @@ -803,7 +802,7 @@
   8.800  fun process_input inp = case inp
   8.801   of Pgip.Askpgip _          => askpgip inp
   8.802    | Pgip.Askpgml _          => askpgml inp
   8.803 -  | Pgip.Askprefs _         => askprefs inp 
   8.804 +  | Pgip.Askprefs _         => askprefs inp
   8.805    | Pgip.Askconfig _        => askconfig inp
   8.806    | Pgip.Getpref _          => getpref inp
   8.807    | Pgip.Setpref _          => setpref inp
   8.808 @@ -843,18 +842,18 @@
   8.809    | Pgip.Quitpgip _         => quitpgip inp
   8.810  
   8.811  
   8.812 -fun process_pgip_element pgipxml = 
   8.813 +fun process_pgip_element pgipxml =
   8.814      case pgipxml of
   8.815 -	(xml as (XML.Elem elem)) =>
   8.816 -	(case Pgip.input elem of
   8.817 -	     NONE => warning ("Unrecognized PGIP command, ignored: \n" ^
   8.818 -			      (XML.string_of_tree xml))
   8.819 -	   | SOME inp => (process_input inp)) (* errors later; packet discarded *)
   8.820 +        (xml as (XML.Elem elem)) =>
   8.821 +        (case Pgip.input elem of
   8.822 +             NONE => warning ("Unrecognized PGIP command, ignored: \n" ^
   8.823 +                              (XML.string_of_tree xml))
   8.824 +           | SOME inp => (process_input inp)) (* errors later; packet discarded *)
   8.825        | (XML.Text t) => ignored_text_warning t
   8.826 -      |	(XML.Rawtext t) => ignored_text_warning t
   8.827 +      | (XML.Rawtext t) => ignored_text_warning t
   8.828  and ignored_text_warning t =
   8.829 -    if (size (Symbol.strip_blanks t) > 0) then
   8.830 -	   warning ("Ignored text in PGIP packet: \n" ^ t)
   8.831 +    if size (Symbol.strip_blanks t) > 0 then
   8.832 +           warning ("Ignored text in PGIP packet: \n" ^ t)
   8.833      else ()
   8.834  
   8.835  fun process_pgip_tree xml =
   8.836 @@ -865,27 +864,27 @@
   8.837            (let
   8.838                 val class = PgipTypes.get_attr "class" attrs
   8.839                 val dest  = PgipTypes.get_attr_opt "destid" attrs
   8.840 -	       val seq = PgipTypes.read_pgipnat (PgipTypes.get_attr "seq" attrs)
   8.841 +               val seq = PgipTypes.read_pgipnat (PgipTypes.get_attr "seq" attrs)
   8.842                 (* Respond to prover broadcasts, or messages for us. Ignore rest *)
   8.843 -	       val processit = 
   8.844 -		   case dest of
   8.845 +               val processit =
   8.846 +                   case dest of
   8.847                         NONE =>    class = "pa"
   8.848 -		     | SOME id => matching_pgip_id id
   8.849 -	   in if processit then
   8.850 -		  (pgip_refid :=  PgipTypes.get_attr_opt "id" attrs;
   8.851 -		   pgip_refseq := SOME seq;
   8.852 -		   List.app process_pgip_element pgips; 
   8.853 -		   (* return true to indicate <ready/> *)
   8.854 -		   true)
   8.855 -	      else 
   8.856 -		  (* no response to ignored messages. *) 
   8.857 -		  false
   8.858 +                     | SOME id => matching_pgip_id id
   8.859 +           in if processit then
   8.860 +                  (pgip_refid :=  PgipTypes.get_attr_opt "id" attrs;
   8.861 +                   pgip_refseq := SOME seq;
   8.862 +                   List.app process_pgip_element pgips;
   8.863 +                   (* return true to indicate <ready/> *)
   8.864 +                   true)
   8.865 +              else
   8.866 +                  (* no response to ignored messages. *)
   8.867 +                  false
   8.868             end)
   8.869          | _ => raise PGIP "Invalid PGIP packet received")
   8.870       handle PGIP msg =>
   8.871              (Output.error_msg ((msg ^ "\nPGIP error occured in XML text below:\n") ^
   8.872 -			       (XML.string_of_tree xml));
   8.873 -	     true))
   8.874 +                               (XML.string_of_tree xml));
   8.875 +             true))
   8.876  
   8.877  (* External input *)
   8.878  
   8.879 @@ -910,8 +909,8 @@
   8.880               NONE  => ()
   8.881             | SOME (pgip,src') =>
   8.882               let
   8.883 -                 val ready' = (process_pgip_tree pgip) 
   8.884 -				handle e => (handler (e,SOME src'); true)
   8.885 +                 val ready' = (process_pgip_tree pgip)
   8.886 +                                handle e => (handler (e,SOME src'); true)
   8.887               in
   8.888                   loop ready' src'
   8.889               end
   8.890 @@ -922,12 +921,12 @@
   8.891          (XML_PARSE,SOME src) =>
   8.892          Output.panic "Invalid XML input, aborting"
   8.893        | (PGIP_QUIT,_) => ()
   8.894 -      | (Interrupt,SOME src) => 
   8.895 -	(Output.error_msg "Interrupt during PGIP processing"; loop true src)
   8.896 -      | (Toplevel.UNDEF,SOME src) => 
   8.897 -	(Output.error_msg "No working context defined"; loop true src)
   8.898 -      | (e,SOME src) => 
   8.899 -	(Output.error_msg (Toplevel.exn_message e); loop true src)
   8.900 +      | (Interrupt,SOME src) =>
   8.901 +        (Output.error_msg "Interrupt during PGIP processing"; loop true src)
   8.902 +      | (Toplevel.UNDEF,SOME src) =>
   8.903 +        (Output.error_msg "No working context defined"; loop true src)
   8.904 +      | (e,SOME src) =>
   8.905 +        (Output.error_msg (Toplevel.exn_message e); loop true src)
   8.906        | (_,NONE) => ()
   8.907  in
   8.908    (* TODO: add socket interface *)
   8.909 @@ -940,7 +939,7 @@
   8.910  end
   8.911  
   8.912  
   8.913 -(* additional outer syntax for Isar *)  
   8.914 +(* additional outer syntax for Isar *)
   8.915  (* da: TODO: perhaps we can drop this superfluous syntax now??
   8.916     Seems cleaner to support the operations directly above in the PGIP actions.
   8.917   *)
   8.918 @@ -1033,11 +1032,11 @@
   8.919  
   8.920  (* Set recipient for PGIP results *)
   8.921  fun init_pgip_channel writefn =
   8.922 -    (init_pgip_session_id();  
   8.923 -     pgip_output_channel := writefn)				  
   8.924 +    (init_pgip_session_id();
   8.925 +     pgip_output_channel := writefn)
   8.926  
   8.927 -(* Process a PGIP command. 
   8.928 -   This works for preferences but not generally guaranteed 
   8.929 +(* Process a PGIP command.
   8.930 +   This works for preferences but not generally guaranteed
   8.931     because we haven't done full setup here (e.g., no pgml mode)  *)
   8.932  fun process_pgip str =
   8.933       setmp output_xml_fn (!pgip_output_channel) process_pgip_plain str
     9.1 --- a/src/Pure/proof_general.ML	Fri Dec 29 18:25:45 2006 +0100
     9.2 +++ b/src/Pure/proof_general.ML	Fri Dec 29 18:25:46 2006 +0100
     9.3 @@ -53,7 +53,6 @@
     9.4  
     9.5  val proof_generalN = "ProofGeneral";  (*token markup (colouring vars, etc.)*)
     9.6  val pgasciiN = "PGASCII";             (*plain 7-bit ASCII communication*)
     9.7 -val xsymbolsN = Symbol.xsymbolsN;     (*X-Symbol symbols*)
     9.8  val pgmlN = "PGML";                   (*XML escapes and PGML symbol elements*)
     9.9  val pgmlatomsN = "PGMLatoms";         (*variable kind decorations*)
    9.10  val thm_depsN = "thm_deps";           (*meta-information about theorem deps*)
    9.11 @@ -73,7 +72,7 @@
    9.12    | xsym_output s = if Symbol.is_raw s then Symbol.decode_raw s else s;
    9.13  
    9.14  fun xsymbols_output s =
    9.15 -  if Output.has_mode xsymbolsN andalso exists_string (equal "\\") s then
    9.16 +  if Output.has_mode Symbol.xsymbolsN andalso exists_string (equal "\\") s then
    9.17      let val syms = Symbol.explode s
    9.18      in (implode (map xsym_output syms), real (Symbol.length syms)) end
    9.19    else Symbol.default_output s;
    9.20 @@ -94,7 +93,7 @@
    9.21  in
    9.22  
    9.23  fun setup_xsymbols_output () =
    9.24 -  Output.add_mode xsymbolsN
    9.25 +  Output.add_mode Symbol.xsymbolsN
    9.26      (xsymbols_output, K xsymbols_output, Symbol.default_indent, Symbol.encode_raw);
    9.27  
    9.28  fun setup_pgml_output () =
    9.29 @@ -314,20 +313,20 @@
    9.30  fun tell_file_loaded path =
    9.31    if pgip () then
    9.32      issue_pgipe "informfileloaded"
    9.33 -      [localfile_url_attr  (XML.text (File.platform_path 
    9.34 -					  (File.full_path path)))]
    9.35 +      [localfile_url_attr  (XML.text (File.platform_path
    9.36 +                                          (File.full_path path)))]
    9.37    else
    9.38 -    emacs_notify ("Proof General, this file is loaded: " ^ 
    9.39 -		  quote (File.platform_path path));
    9.40 +    emacs_notify ("Proof General, this file is loaded: " ^
    9.41 +                  quote (File.platform_path path));
    9.42  
    9.43  fun tell_file_retracted path =
    9.44    if pgip() then
    9.45      issue_pgipe "informfileretracted"
    9.46 -      [localfile_url_attr  (XML.text (File.platform_path 
    9.47 -					  (File.full_path path)))]
    9.48 +      [localfile_url_attr  (XML.text (File.platform_path
    9.49 +                                          (File.full_path path)))]
    9.50    else
    9.51 -    emacs_notify ("Proof General, you can unlock the file " 
    9.52 -		  ^ quote (File.platform_path path));
    9.53 +    emacs_notify ("Proof General, you can unlock the file "
    9.54 +                  ^ quote (File.platform_path path));
    9.55  
    9.56  
    9.57  (* theory / proof state output *)
    9.58 @@ -618,21 +617,21 @@
    9.59         ("Track theorem dependencies within Proof General",
    9.60          thm_deps_option)),
    9.61       ("skip-proofs",
    9.62 -      ("Ignore proof scripts (interactive-only)",
    9.63 +      ("Skip over proofs (interactive-only)",
    9.64         bool_option Toplevel.skip_proofs))])
    9.65     ];
    9.66  end;
    9.67  
    9.68  (** lexicalstructure element with keywords (PGIP version of elisp keywords file) **)
    9.69  
    9.70 -fun lexicalstructure_keywords () = 
    9.71 +fun lexicalstructure_keywords () =
    9.72      let val commands = OuterSyntax.dest_keywords ()
    9.73 -	fun category_of k = if (k mem commands) then "major" else "minor"
    9.74 +        fun category_of k = if (k mem commands) then "major" else "minor"
    9.75           (* NB: we might filter to only include words like elisp case (OuterSyntax.is_keyword). *)
    9.76 -    	fun keyword_elt (keyword,help,kind,_) = 
    9.77 -  	    XML.element "keyword" [("word", keyword), ("category", category_of kind)]
    9.78 -	  	    [XML.element "shorthelp" [] [XML.text help]]
    9.79 -        in 	    	    
    9.80 +        fun keyword_elt (keyword,help,kind,_) =
    9.81 +            XML.element "keyword" [("word", keyword), ("category", category_of kind)]
    9.82 +                    [XML.element "shorthelp" [] [XML.text help]]
    9.83 +        in
    9.84              (* Also, note we don't call init_outer_syntax here to add interface commands,
    9.85              but they should never appear in scripts anyway so it shouldn't matter *)
    9.86              XML.element "lexicalstructure" [] (map keyword_elt (OuterSyntax.dest_parsers()))
    9.87 @@ -657,18 +656,18 @@
    9.88          val exists = File.exists path
    9.89          val proverinfo =
    9.90              XML.element "proverinfo"
    9.91 -              [("name",     	 "Isabelle"), 
    9.92 -	       ("version",  	 version),
    9.93 -	       ("instance", 	 Session.name()), 
    9.94 -	       ("descr",	 "The Isabelle/Isar theorem prover"),
    9.95 -	       ("url",      	 isabelle_www()),   
    9.96 -	       ("filenameextns", ".thy;")]
    9.97 +              [("name",          "Isabelle"),
    9.98 +               ("version",       version),
    9.99 +               ("instance",      Session.name()),
   9.100 +               ("descr",         "The Isabelle/Isar theorem prover"),
   9.101 +               ("url",           isabelle_www()),
   9.102 +               ("filenameextns", ".thy;")]
   9.103              []
   9.104      in
   9.105          if exists then
   9.106 -            (issue_pgips [proverinfo]; 
   9.107 -	     issue_pgips [File.read path];
   9.108 -	     issue_pgips [lexicalstructure_keywords()])
   9.109 +            (issue_pgips [proverinfo];
   9.110 +             issue_pgips [File.read path];
   9.111 +             issue_pgips [lexicalstructure_keywords()])
   9.112          else Output.panic ("PGIP configuration file \"" ^ config_file() ^ "\" not found")
   9.113      end;
   9.114  end
   9.115 @@ -1257,8 +1256,8 @@
   9.116       | "closegoal"      => isarscript data
   9.117       | "giveupgoal"     => isarscript data
   9.118       | "postponegoal"   => isarscript data
   9.119 -     | "comment"        => isarscript data  
   9.120 -     | "doccomment"     => isarscript data  
   9.121 +     | "comment"        => isarscript data
   9.122 +     | "doccomment"     => isarscript data
   9.123       | "whitespace"     => isarscript data  (* NB: should be ignored, but process anyway *)
   9.124       | "litcomment"     => isarscript data  (* NB: should be ignored, process for back compat *)
   9.125       | "spuriouscmd"    => isarscript data
   9.126 @@ -1303,14 +1302,14 @@
   9.127       | "openfile"       => (case !currently_open_file of
   9.128                                  SOME f => raise PGIP ("openfile when a file is already open!")
   9.129                                | NONE => (openfile_retract (fileurl_of attrs);
   9.130 -					 currently_open_file := SOME (fileurl_of attrs)))
   9.131 +                                         currently_open_file := SOME (fileurl_of attrs)))
   9.132       | "closefile"      => (case !currently_open_file of
   9.133                                  SOME f => (proper_inform_file_processed f (Isar.state());
   9.134                                             currently_open_file := NONE)
   9.135                                | NONE => raise PGIP ("closefile when no file is open!"))
   9.136       | "abortfile"      => (case !currently_open_file of
   9.137                                  SOME f => (isarcmd "init_toplevel";
   9.138 -					   currently_open_file := NONE)
   9.139 +                                           currently_open_file := NONE)
   9.140                                | NONE => raise PGIP ("abortfile when no file is open!"))
   9.141       | "retractfile"    => (case !currently_open_file of
   9.142                                  SOME f => raise PGIP ("retractfile when a file is open!")