# HG changeset patch # User aspinall # Date 1094163978 -7200 # Node ID e1582a0d29b5ecde30dde9e64c80e0f9a281d56f # Parent 73069e033a0b581270cf152061519d18c6918afa Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult. diff -r 73069e033a0b -r e1582a0d29b5 src/Pure/proof_general.ML --- a/src/Pure/proof_general.ML Thu Sep 02 16:52:21 2004 +0200 +++ b/src/Pure/proof_general.ML Fri Sep 03 00:26:18 2004 +0200 @@ -7,14 +7,12 @@ =========================================================================== NOTE: With this version you will lose support for the Isabelle -preferences menu in the currently released version of Proof General (3.5). +settings menu in the currently released version of Proof General (3.5). No other changes should be visible in the Emacs interface. -If the loss of preferences is a serious problem, please use a "sticky" -check-out of the previous version of this file, version 1.27. - -A version of Emacs Proof General which supports the new PGIP format for -preferences will be available shortly. +The 3.6pre pre-release versions of Emacs Proof General now support the +new PGIP format for preferences and restore the settings menu. +Please visit http://proofgeneral.inf.ed.ac.uk/develdownload =========================================================================== STATUS: this version is an experimental version that supports PGIP 2.X. @@ -203,7 +201,13 @@ fun assemble_pgipe resp attrs = assemble_pgips [XML.element resp attrs []] (* FIXME: need to add stuff to gather PGIPs here *) - fun issue_pgip resp attrs = writeln_default o (assemble_pgip resp attrs) + fun issue_pgip resp attrs txt = + if pgip_emacs_compatibility() then + decorated_output (* add urgent message annotation *) + (oct_char "360") (oct_char "361") "" + (assemble_pgip resp attrs txt) + else + writeln_default (assemble_pgip resp attrs txt) (* FIXME: temporarily to support PG 3.4. *) fun issue_pgip_maybe_decorated bg en resp attrs s = @@ -219,12 +223,27 @@ (* messages and notification *) -fun message resp attrs bg en prfx s = - if pgip() then - issue_pgip_maybe_decorated bg en resp attrs (prefix_lines prfx s) - else - decorated_output bg en prfx s; +local + val delay_msgs = ref false (* whether to accumulate messages *) + val delayed_msgs = ref [] +in + fun message resp attrs bg en prfx s = + if pgip() then + (if (!delay_msgs) then + delayed_msgs := (resp,attrs,prefix_lines prfx s)::(!delayed_msgs) (* nb: no decs *) + else + issue_pgip_maybe_decorated bg en resp attrs (prefix_lines prfx s)) + else + decorated_output bg en prfx s; + + fun start_delay_msgs () = (delay_msgs := true; + delayed_msgs := []) + + fun end_delayed_msgs () = + (delay_msgs := false; + map (fn (resp,attrs,s) => XML.element resp attrs [s]) (!delayed_msgs)) +end local val display_area = ("area", "display") @@ -316,9 +335,7 @@ (XML.element "pgml" [] [XML.element "statedisplay" [] - [Output.output (* FIXME: needed? *) - (Pretty.output - (Pretty.chunks prts))]]) + [(Pretty.output (Pretty.chunks prts))]]) fun print_current_goals n m st = if pgml () then statedisplay (Display.pretty_current_goals n m st) @@ -493,24 +510,24 @@ fun nat_option r = (pgipnat, withdefault (fn () => string_of_int (!r)), (fn s => (case Syntax.read_nat s of - None => error "nat_option: illegal value" + None => error ("nat_option: illegal value " ^ s) | Some i => r := i))); fun bool_option r = (pgipbool, withdefault (fn () => Bool.toString (!r)), (fn "false" => r := false | "true" => r := true - | _ => error "bool_option: illegal value")); + | x => error ("bool_option: illegal value" ^ x))); val proof_option = (pgipbool, withdefault (fn () => Bool.toString (!proofs >= 2)), (fn "false" => proofs := 1 | "true" => proofs := 2 - | _ => error "proof_option: illegal value")); + | x => error ("proof_option: illegal value" ^ x))); val thm_deps_option = (pgipbool, withdefault (fn () => Bool.toString (Output.has_mode "thm_deps")), (fn "false" => print_mode := ((!print_mode) \ "thm_deps") | "true" => print_mode := ("thm_deps" ins (!print_mode)) - | _ => error "thm_deps_option: illegal value")); + | x => error ("thm_deps_option: illegal value " ^ x))); local val pg_print_depth_val = ref 10 @@ -519,7 +536,7 @@ val print_depth_option = (pgipnat, withdefault (fn () => string_of_int (!pg_print_depth_val)), (fn s => (case Syntax.read_nat s of - None => error "print_depth_option: illegal value" + None => error ("print_depth_option: illegal value" ^ s) | Some i => pg_print_depth i))) end @@ -751,7 +768,8 @@ let val ((thyname,imports,files),_) = ThyHeader.args (toks@sync) in - markup_text_attrs str "opentheory" [("thyname",thyname)] + markup_text_attrs str "opentheory" [("thyname",thyname), + ("parentnames", space_implode ";" imports)] end fun xmls_of_thy_decl (name,toks,str) = (* see isar_syn.ML/thy_decl cases *) @@ -890,6 +908,8 @@ (markup whs "comment") @ (markup rest "unparseable") end +fun markup_unparseable str = markup_text str "unparseable" + end @@ -905,10 +925,7 @@ in fun xmls_of_str str = let - val toks = OuterSyntax.scan str - (* parsing: See outer_syntax.ML/toplevel_source *) - fun parse_loop ([],[],xmls) = xmls | parse_loop ([],itoks,xmls) = xmls @ (xmls_of_impropers itoks) | parse_loop ((nm,toks,_)::trs,itoks,xmls) = @@ -928,14 +945,22 @@ parse_loop(trs,itoks'',xmls @ xmls_whs @ xmls_tr) end in - (* FIXME: put errors/warnings inside the parse result *) - parse_loop (OuterSyntax.read toks, toks, []) + (let val toks = OuterSyntax.scan str + in + parse_loop (OuterSyntax.read toks, toks, []) + end) + handle _ => markup_unparseable str end -fun parsescript str = - issue_pgips [XML.element "parseresult" [] (xmls_of_str str)] - +fun parsescript str attrs = + let + val _ = start_delay_msgs () (* accumulate error messages to put inside parseresult *) + val xmls = xmls_of_str str + val errs = end_delayed_msgs () + in + issue_pgips [XML.element "parseresult" attrs (errs@xmls)] + end end @@ -1010,69 +1035,48 @@ end -local - (* Proof control commands *) +(* Proof control commands *) - fun xmlattro attrs attr = assoc(attrs,attr) +local + fun xmlattro attr attrs = assoc(attrs,attr) - fun xmlattr attrs attr = - (case xmlattro attrs attr of + fun xmlattr attr attrs = + (case xmlattro attr attrs of Some value => value | None => raise PGIP ("Missing attribute: " ^ attr)) - val thyname_attr = "thyname" - val objtype_attr = "objtype" - val name_attr = "name" - val dirname_attr = "dir" + val thyname_attro = xmlattro "thyname" + val thyname_attr = xmlattr "thyname" + val objtype_attro = xmlattro "objtype" + val objtype_attr = xmlattr "objtype" + val name_attr = xmlattr "name" + val dirname_attr = xmlattr "dir" fun comment x = "(* " ^ x ^ " *)" - (* parse URLs like "file://host/name.thy" *) - (* FIXME: instead of this, extend code in General/url.ML & use that. *) - fun decode_url url = - (let - val sep = find_index_eq ":" (explode url) - val proto = String.substring(url,0,sep) - val hostsep = find_index_eq "/" (drop (sep+3,explode url)) - val host = String.substring(url,sep+3,hostsep-sep+4) - val doc = if (size url >= sep+hostsep+3) then - String.substring(url,sep+hostsep+4,size url-hostsep-sep-4) - else "" - in - (proto,host,doc) - end) handle Subscript => error ("Badly formed URL " ^ url) - - fun localfile_of_url url = - let - val (proto,host,name) = decode_url url - in - if (proto = "file" andalso - (host = "" orelse - host = "localhost" orelse - host = (getenv "HOSTNAME"))) - then name - else error ("Cannot access non-local URL " ^ url) - end + fun localfile_of_url url = (* only handle file:/// or file://localhost/ *) + case Url.unpack url of + (Url.File path) => File.sysify_path path + | _ => error ("Cannot access non-local URL " ^ url) - fun fileurl_of attrs = localfile_of_url (xmlattr attrs "url") + val fileurl_of = localfile_of_url o (xmlattr "url") val topthy = Toplevel.theory_of o Toplevel.get_state val topthy_name = PureThy.get_name o topthy val currently_open_file = ref (None : string option) - in fun process_pgip_element pgipxml = (case pgipxml of (XML.Text t) => warning ("Ignored text in PGIP packet: \n" ^ t) -| (XML.Elem (xml as (elem, attrs, data))) => +| (xml as (XML.Elem (elem, attrs, data))) => (case elem of (* protocol config *) "askpgip" => (usespgip (); send_pgip_config ()) | "askpgml" => usespgml () (* proverconfig *) | "askprefs" => hasprefs () - | "getpref" => getpref (xmlattr attrs name_attr) - | "setpref" => setpref (xmlattr attrs name_attr) (xmltext data) + | "getpref" => getpref (name_attr attrs) + | "setpref" => setpref (name_attr attrs) (xmltext data) (* provercontrol *) | "proverinit" => isar_restart () | "proverexit" => isarcmd "quit" @@ -1098,12 +1102,9 @@ | "forget" => error "Not implemented" | "restoregoal" => error "Not implemented" (* could just treat as forget? *) (* proofctxt: improper commands *) - | "askids" => askids (xmlattro attrs thyname_attr, - xmlattro attrs objtype_attr) - | "showid" => showid (xmlattro attrs thyname_attr, - xmlattr attrs objtype_attr, - xmlattr attrs name_attr) - | "parsescript" => parsescript (xmltext data) + | "askids" => askids (thyname_attro attrs, objtype_attro attrs) + | "showid" => showid (thyname_attro attrs, objtype_attr attrs, name_attr attrs) + | "parsescript" => parsescript (xmltext data) attrs (* just pass back attrs unchanged *) | "showproofstate" => isarcmd "pr" | "showctxt" => isarcmd "print_theory" (* more useful than print_context *) | "searchtheorems" => isarcmd ("thms_containing " ^ (xmltext data)) @@ -1116,9 +1117,8 @@ writeln ("Theory "^(topthy_name())^" completed.")) (* improperfilecmd: theory-level commands not in script *) | "aborttheory" => isarcmd ("init_toplevel") - | "retracttheory" => isarcmd ("kill_thy " ^ - (quote (xmlattr attrs thyname_attr))) - | "loadfile" => use_thy_or_ml_file (fileurl_of attrs) + | "retracttheory" => isarcmd ("kill_thy " ^ (quote (thyname_attr attrs))) + | "loadfile" => use_thy_or_ml_file (fileurl_of attrs) | "openfile" => (inform_file_retracted (fileurl_of attrs); currently_open_file := Some (fileurl_of attrs)) | "closefile" => (case !currently_open_file of @@ -1126,21 +1126,21 @@ currently_open_file := None) | None => raise PGIP ("closefile when no file is open!")) | "abortfile" => (currently_open_file := None) (* perhaps error for no file open *) - | "changecwd" => ThyLoad.add_path (xmlattr attrs dirname_attr) + | "changecwd" => ThyLoad.add_path (dirname_attr attrs) | "systemcmd" => isarscript data (* unofficial command for debugging *) | "quitpgip" => raise PGIP_QUIT | _ => raise PGIP ("Unrecognized PGIP element: " ^ elem))) -fun process_pgip_tree s = +fun process_pgip_tree xml = (pgip_refseq := None; pgip_refid := None; - (case s of + (case xml of XML.Elem ("pgip", attrs, pgips) => (let - val class = xmlattr attrs "class" - val _ = (pgip_refseq := xmlattro attrs "seq"; - pgip_refid := xmlattro attrs "id") + val class = xmlattr "class" attrs + val _ = (pgip_refseq := xmlattro "seq" attrs; + pgip_refid := xmlattro "id" attrs) in if (class = "pa") then seq process_pgip_element pgips @@ -1150,7 +1150,7 @@ | _ => raise PGIP "Invalid PGIP packet received") handle (PGIP msg) => (error (msg ^ "\nPGIP error occured in XML text below:\n" ^ - (XML.string_of_tree s)))) + (XML.string_of_tree xml)))) (* for export to Emacs *) (* val process_pgip = process_pgip_tree o XML.tree_of_string; *)