Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
1.1 --- a/src/Pure/proof_general.ML Thu Sep 02 16:52:21 2004 +0200
1.2 +++ b/src/Pure/proof_general.ML Fri Sep 03 00:26:18 2004 +0200
1.3 @@ -7,14 +7,12 @@
1.4
1.5 ===========================================================================
1.6 NOTE: With this version you will lose support for the Isabelle
1.7 -preferences menu in the currently released version of Proof General (3.5).
1.8 +settings menu in the currently released version of Proof General (3.5).
1.9 No other changes should be visible in the Emacs interface.
1.10
1.11 -If the loss of preferences is a serious problem, please use a "sticky"
1.12 -check-out of the previous version of this file, version 1.27.
1.13 -
1.14 -A version of Emacs Proof General which supports the new PGIP format for
1.15 -preferences will be available shortly.
1.16 +The 3.6pre pre-release versions of Emacs Proof General now support the
1.17 +new PGIP format for preferences and restore the settings menu.
1.18 +Please visit http://proofgeneral.inf.ed.ac.uk/develdownload
1.19 ===========================================================================
1.20
1.21 STATUS: this version is an experimental version that supports PGIP 2.X.
1.22 @@ -203,7 +201,13 @@
1.23 fun assemble_pgipe resp attrs = assemble_pgips [XML.element resp attrs []]
1.24
1.25 (* FIXME: need to add stuff to gather PGIPs here *)
1.26 - fun issue_pgip resp attrs = writeln_default o (assemble_pgip resp attrs)
1.27 + fun issue_pgip resp attrs txt =
1.28 + if pgip_emacs_compatibility() then
1.29 + decorated_output (* add urgent message annotation *)
1.30 + (oct_char "360") (oct_char "361") ""
1.31 + (assemble_pgip resp attrs txt)
1.32 + else
1.33 + writeln_default (assemble_pgip resp attrs txt)
1.34
1.35 (* FIXME: temporarily to support PG 3.4. *)
1.36 fun issue_pgip_maybe_decorated bg en resp attrs s =
1.37 @@ -219,12 +223,27 @@
1.38
1.39 (* messages and notification *)
1.40
1.41 -fun message resp attrs bg en prfx s =
1.42 - if pgip() then
1.43 - issue_pgip_maybe_decorated bg en resp attrs (prefix_lines prfx s)
1.44 - else
1.45 - decorated_output bg en prfx s;
1.46 +local
1.47 + val delay_msgs = ref false (* whether to accumulate messages *)
1.48 + val delayed_msgs = ref []
1.49 +in
1.50
1.51 + fun message resp attrs bg en prfx s =
1.52 + if pgip() then
1.53 + (if (!delay_msgs) then
1.54 + delayed_msgs := (resp,attrs,prefix_lines prfx s)::(!delayed_msgs) (* nb: no decs *)
1.55 + else
1.56 + issue_pgip_maybe_decorated bg en resp attrs (prefix_lines prfx s))
1.57 + else
1.58 + decorated_output bg en prfx s;
1.59 +
1.60 + fun start_delay_msgs () = (delay_msgs := true;
1.61 + delayed_msgs := [])
1.62 +
1.63 + fun end_delayed_msgs () =
1.64 + (delay_msgs := false;
1.65 + map (fn (resp,attrs,s) => XML.element resp attrs [s]) (!delayed_msgs))
1.66 +end
1.67
1.68 local
1.69 val display_area = ("area", "display")
1.70 @@ -316,9 +335,7 @@
1.71 (XML.element "pgml" []
1.72 [XML.element "statedisplay"
1.73 []
1.74 - [Output.output (* FIXME: needed? *)
1.75 - (Pretty.output
1.76 - (Pretty.chunks prts))]])
1.77 + [(Pretty.output (Pretty.chunks prts))]])
1.78
1.79 fun print_current_goals n m st =
1.80 if pgml () then statedisplay (Display.pretty_current_goals n m st)
1.81 @@ -493,24 +510,24 @@
1.82 fun nat_option r = (pgipnat,
1.83 withdefault (fn () => string_of_int (!r)),
1.84 (fn s => (case Syntax.read_nat s of
1.85 - None => error "nat_option: illegal value"
1.86 + None => error ("nat_option: illegal value " ^ s)
1.87 | Some i => r := i)));
1.88
1.89 fun bool_option r = (pgipbool,
1.90 withdefault (fn () => Bool.toString (!r)),
1.91 (fn "false" => r := false | "true" => r := true
1.92 - | _ => error "bool_option: illegal value"));
1.93 + | x => error ("bool_option: illegal value" ^ x)));
1.94
1.95 val proof_option = (pgipbool,
1.96 withdefault (fn () => Bool.toString (!proofs >= 2)),
1.97 (fn "false" => proofs := 1 | "true" => proofs := 2
1.98 - | _ => error "proof_option: illegal value"));
1.99 + | x => error ("proof_option: illegal value" ^ x)));
1.100
1.101 val thm_deps_option = (pgipbool,
1.102 withdefault (fn () => Bool.toString (Output.has_mode "thm_deps")),
1.103 (fn "false" => print_mode := ((!print_mode) \ "thm_deps")
1.104 | "true" => print_mode := ("thm_deps" ins (!print_mode))
1.105 - | _ => error "thm_deps_option: illegal value"));
1.106 + | x => error ("thm_deps_option: illegal value " ^ x)));
1.107
1.108 local
1.109 val pg_print_depth_val = ref 10
1.110 @@ -519,7 +536,7 @@
1.111 val print_depth_option = (pgipnat,
1.112 withdefault (fn () => string_of_int (!pg_print_depth_val)),
1.113 (fn s => (case Syntax.read_nat s of
1.114 - None => error "print_depth_option: illegal value"
1.115 + None => error ("print_depth_option: illegal value" ^ s)
1.116 | Some i => pg_print_depth i)))
1.117 end
1.118
1.119 @@ -751,7 +768,8 @@
1.120 let
1.121 val ((thyname,imports,files),_) = ThyHeader.args (toks@sync)
1.122 in
1.123 - markup_text_attrs str "opentheory" [("thyname",thyname)]
1.124 + markup_text_attrs str "opentheory" [("thyname",thyname),
1.125 + ("parentnames", space_implode ";" imports)]
1.126 end
1.127
1.128 fun xmls_of_thy_decl (name,toks,str) = (* see isar_syn.ML/thy_decl cases *)
1.129 @@ -890,6 +908,8 @@
1.130 (markup whs "comment") @ (markup rest "unparseable")
1.131 end
1.132
1.133 +fun markup_unparseable str = markup_text str "unparseable"
1.134 +
1.135 end
1.136
1.137
1.138 @@ -905,10 +925,7 @@
1.139 in
1.140 fun xmls_of_str str =
1.141 let
1.142 - val toks = OuterSyntax.scan str
1.143 -
1.144 (* parsing: See outer_syntax.ML/toplevel_source *)
1.145 -
1.146 fun parse_loop ([],[],xmls) = xmls
1.147 | parse_loop ([],itoks,xmls) = xmls @ (xmls_of_impropers itoks)
1.148 | parse_loop ((nm,toks,_)::trs,itoks,xmls) =
1.149 @@ -928,14 +945,22 @@
1.150 parse_loop(trs,itoks'',xmls @ xmls_whs @ xmls_tr)
1.151 end
1.152 in
1.153 - (* FIXME: put errors/warnings inside the parse result *)
1.154 - parse_loop (OuterSyntax.read toks, toks, [])
1.155 + (let val toks = OuterSyntax.scan str
1.156 + in
1.157 + parse_loop (OuterSyntax.read toks, toks, [])
1.158 + end)
1.159 + handle _ => markup_unparseable str
1.160 end
1.161
1.162
1.163 -fun parsescript str =
1.164 - issue_pgips [XML.element "parseresult" [] (xmls_of_str str)]
1.165 -
1.166 +fun parsescript str attrs =
1.167 + let
1.168 + val _ = start_delay_msgs () (* accumulate error messages to put inside parseresult *)
1.169 + val xmls = xmls_of_str str
1.170 + val errs = end_delayed_msgs ()
1.171 + in
1.172 + issue_pgips [XML.element "parseresult" attrs (errs@xmls)]
1.173 + end
1.174 end
1.175
1.176
1.177 @@ -1010,69 +1035,48 @@
1.178 end
1.179
1.180
1.181 +(* Proof control commands *)
1.182 +
1.183 local
1.184 - (* Proof control commands *)
1.185 + fun xmlattro attr attrs = assoc(attrs,attr)
1.186
1.187 - fun xmlattro attrs attr = assoc(attrs,attr)
1.188 -
1.189 - fun xmlattr attrs attr =
1.190 - (case xmlattro attrs attr of
1.191 + fun xmlattr attr attrs =
1.192 + (case xmlattro attr attrs of
1.193 Some value => value
1.194 | None => raise PGIP ("Missing attribute: " ^ attr))
1.195
1.196 - val thyname_attr = "thyname"
1.197 - val objtype_attr = "objtype"
1.198 - val name_attr = "name"
1.199 - val dirname_attr = "dir"
1.200 + val thyname_attro = xmlattro "thyname"
1.201 + val thyname_attr = xmlattr "thyname"
1.202 + val objtype_attro = xmlattro "objtype"
1.203 + val objtype_attr = xmlattr "objtype"
1.204 + val name_attr = xmlattr "name"
1.205 + val dirname_attr = xmlattr "dir"
1.206 fun comment x = "(* " ^ x ^ " *)"
1.207
1.208 - (* parse URLs like "file://host/name.thy" *)
1.209 - (* FIXME: instead of this, extend code in General/url.ML & use that. *)
1.210 - fun decode_url url =
1.211 - (let
1.212 - val sep = find_index_eq ":" (explode url)
1.213 - val proto = String.substring(url,0,sep)
1.214 - val hostsep = find_index_eq "/" (drop (sep+3,explode url))
1.215 - val host = String.substring(url,sep+3,hostsep-sep+4)
1.216 - val doc = if (size url >= sep+hostsep+3) then
1.217 - String.substring(url,sep+hostsep+4,size url-hostsep-sep-4)
1.218 - else ""
1.219 - in
1.220 - (proto,host,doc)
1.221 - end) handle Subscript => error ("Badly formed URL " ^ url)
1.222 -
1.223 - fun localfile_of_url url =
1.224 - let
1.225 - val (proto,host,name) = decode_url url
1.226 - in
1.227 - if (proto = "file" andalso
1.228 - (host = "" orelse
1.229 - host = "localhost" orelse
1.230 - host = (getenv "HOSTNAME")))
1.231 - then name
1.232 - else error ("Cannot access non-local URL " ^ url)
1.233 - end
1.234 + fun localfile_of_url url = (* only handle file:/// or file://localhost/ *)
1.235 + case Url.unpack url of
1.236 + (Url.File path) => File.sysify_path path
1.237 + | _ => error ("Cannot access non-local URL " ^ url)
1.238
1.239 - fun fileurl_of attrs = localfile_of_url (xmlattr attrs "url")
1.240 + val fileurl_of = localfile_of_url o (xmlattr "url")
1.241
1.242 val topthy = Toplevel.theory_of o Toplevel.get_state
1.243 val topthy_name = PureThy.get_name o topthy
1.244
1.245 val currently_open_file = ref (None : string option)
1.246 -
1.247 in
1.248
1.249 fun process_pgip_element pgipxml = (case pgipxml of
1.250 (XML.Text t) => warning ("Ignored text in PGIP packet: \n" ^ t)
1.251 -| (XML.Elem (xml as (elem, attrs, data))) =>
1.252 +| (xml as (XML.Elem (elem, attrs, data))) =>
1.253 (case elem of
1.254 (* protocol config *)
1.255 "askpgip" => (usespgip (); send_pgip_config ())
1.256 | "askpgml" => usespgml ()
1.257 (* proverconfig *)
1.258 | "askprefs" => hasprefs ()
1.259 - | "getpref" => getpref (xmlattr attrs name_attr)
1.260 - | "setpref" => setpref (xmlattr attrs name_attr) (xmltext data)
1.261 + | "getpref" => getpref (name_attr attrs)
1.262 + | "setpref" => setpref (name_attr attrs) (xmltext data)
1.263 (* provercontrol *)
1.264 | "proverinit" => isar_restart ()
1.265 | "proverexit" => isarcmd "quit"
1.266 @@ -1098,12 +1102,9 @@
1.267 | "forget" => error "Not implemented"
1.268 | "restoregoal" => error "Not implemented" (* could just treat as forget? *)
1.269 (* proofctxt: improper commands *)
1.270 - | "askids" => askids (xmlattro attrs thyname_attr,
1.271 - xmlattro attrs objtype_attr)
1.272 - | "showid" => showid (xmlattro attrs thyname_attr,
1.273 - xmlattr attrs objtype_attr,
1.274 - xmlattr attrs name_attr)
1.275 - | "parsescript" => parsescript (xmltext data)
1.276 + | "askids" => askids (thyname_attro attrs, objtype_attro attrs)
1.277 + | "showid" => showid (thyname_attro attrs, objtype_attr attrs, name_attr attrs)
1.278 + | "parsescript" => parsescript (xmltext data) attrs (* just pass back attrs unchanged *)
1.279 | "showproofstate" => isarcmd "pr"
1.280 | "showctxt" => isarcmd "print_theory" (* more useful than print_context *)
1.281 | "searchtheorems" => isarcmd ("thms_containing " ^ (xmltext data))
1.282 @@ -1116,9 +1117,8 @@
1.283 writeln ("Theory "^(topthy_name())^" completed."))
1.284 (* improperfilecmd: theory-level commands not in script *)
1.285 | "aborttheory" => isarcmd ("init_toplevel")
1.286 - | "retracttheory" => isarcmd ("kill_thy " ^
1.287 - (quote (xmlattr attrs thyname_attr)))
1.288 - | "loadfile" => use_thy_or_ml_file (fileurl_of attrs)
1.289 + | "retracttheory" => isarcmd ("kill_thy " ^ (quote (thyname_attr attrs)))
1.290 + | "loadfile" => use_thy_or_ml_file (fileurl_of attrs)
1.291 | "openfile" => (inform_file_retracted (fileurl_of attrs);
1.292 currently_open_file := Some (fileurl_of attrs))
1.293 | "closefile" => (case !currently_open_file of
1.294 @@ -1126,21 +1126,21 @@
1.295 currently_open_file := None)
1.296 | None => raise PGIP ("closefile when no file is open!"))
1.297 | "abortfile" => (currently_open_file := None) (* perhaps error for no file open *)
1.298 - | "changecwd" => ThyLoad.add_path (xmlattr attrs dirname_attr)
1.299 + | "changecwd" => ThyLoad.add_path (dirname_attr attrs)
1.300 | "systemcmd" => isarscript data
1.301 (* unofficial command for debugging *)
1.302 | "quitpgip" => raise PGIP_QUIT
1.303 | _ => raise PGIP ("Unrecognized PGIP element: " ^ elem)))
1.304
1.305 -fun process_pgip_tree s =
1.306 +fun process_pgip_tree xml =
1.307 (pgip_refseq := None;
1.308 pgip_refid := None;
1.309 - (case s of
1.310 + (case xml of
1.311 XML.Elem ("pgip", attrs, pgips) =>
1.312 (let
1.313 - val class = xmlattr attrs "class"
1.314 - val _ = (pgip_refseq := xmlattro attrs "seq";
1.315 - pgip_refid := xmlattro attrs "id")
1.316 + val class = xmlattr "class" attrs
1.317 + val _ = (pgip_refseq := xmlattro "seq" attrs;
1.318 + pgip_refid := xmlattro "id" attrs)
1.319 in
1.320 if (class = "pa") then
1.321 seq process_pgip_element pgips
1.322 @@ -1150,7 +1150,7 @@
1.323 | _ => raise PGIP "Invalid PGIP packet received")
1.324 handle (PGIP msg) =>
1.325 (error (msg ^ "\nPGIP error occured in XML text below:\n" ^
1.326 - (XML.string_of_tree s))))
1.327 + (XML.string_of_tree xml))))
1.328
1.329 (* for export to Emacs *)
1.330 (* val process_pgip = process_pgip_tree o XML.tree_of_string; *)