1.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML Mon May 13 20:26:34 2013 +0200
1.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Mon May 13 20:30:49 2013 +0200
1.3 @@ -11,12 +11,6 @@
1.4
1.5 val new_thms_deps: theory -> theory -> string list * string list
1.6
1.7 - (* More message functions... *)
1.8 - val nonfatal_error : string -> unit (* recoverable (batch) error: carry on scripting *)
1.9 - val log_msg : string -> unit (* for internal log messages *)
1.10 - val error_with_pos : PgipTypes.displayarea -> PgipTypes.fatality -> Position.T -> string -> unit
1.11 -
1.12 - val get_currently_open_file : unit -> Path.T option (* interface focus *)
1.13 val add_preference: string -> Preferences.preference -> unit
1.14 end
1.15
1.16 @@ -32,8 +26,6 @@
1.17 (** print mode **)
1.18
1.19 val proof_general_emacsN = "ProofGeneralEmacs";
1.20 -val proof_generalN = "ProofGeneral";
1.21 -val pgmlsymbols_flag = Unsynchronized.ref true;
1.22
1.23
1.24 (* assembling and issuing PGIP packets *)
1.25 @@ -62,183 +54,12 @@
1.26
1.27 fun matching_pgip_id id = (id = pgip_id)
1.28
1.29 -val output_xml_fn = Unsynchronized.ref Output.physical_writeln
1.30 -fun output_xml s = ! output_xml_fn (XML.string_of s);
1.31 -
1.32 val output_pgips = XML.string_of o PgipOutput.output o assemble_pgips o map PgipOutput.output;
1.33
1.34 -val output_pgmlterm = XML.string_of o Pgml.pgmlterm_to_xml;
1.35 -val output_pgmltext = XML.string_of o Pgml.pgml_to_xml;
1.36 -
1.37 -
1.38 -fun issue_pgip_rawtext str =
1.39 - output_xml (PgipOutput.output (assemble_pgips (YXML.parse_body str)));
1.40 -
1.41 -fun issue_pgip pgipop =
1.42 - output_xml (PgipOutput.output (assemble_pgips [PgipOutput.output pgipop]));
1.43 -
1.44 end;
1.45
1.46
1.47
1.48 -(** messages and notification **)
1.49 -
1.50 -(* PGML terms *)
1.51 -
1.52 -local
1.53 -
1.54 -fun pgml_sym s =
1.55 - if ! pgmlsymbols_flag then
1.56 - (case Symbol.decode s of
1.57 - Symbol.Sym name => Pgml.Sym {name = name, content = s}
1.58 - | _ => Pgml.Str s)
1.59 - else Pgml.Str s;
1.60 -
1.61 -val pgml_syms = map pgml_sym o Symbol.explode;
1.62 -
1.63 -val token_markups =
1.64 - [Markup.tfreeN, Markup.tvarN, Markup.freeN, Markup.boundN, Markup.varN, Markup.skolemN];
1.65 -
1.66 -fun get_int props name =
1.67 - (case Properties.get props name of NONE => NONE | SOME s => Int.fromString s);
1.68 -
1.69 -in
1.70 -
1.71 -fun pgml_terms (XML.Elem ((name, atts), body)) =
1.72 - if member (op =) token_markups name then
1.73 - let val content = pgml_syms (XML.content_of body)
1.74 - in [Pgml.Atoms {kind = SOME name, content = content}] end
1.75 - else
1.76 - let val content = maps pgml_terms body in
1.77 - if name = Markup.blockN then
1.78 - [Pgml.Box {orient = NONE, indent = get_int atts Markup.indentN, content = content}]
1.79 - else if name = Markup.breakN then
1.80 - [Pgml.Break {mandatory = NONE, indent = get_int atts Markup.widthN}]
1.81 - else content
1.82 - end
1.83 - | pgml_terms (XML.Text text) = map (Pgml.Raw o Pgml.atom_to_xml) (pgml_syms text);
1.84 -
1.85 -end;
1.86 -
1.87 -
1.88 -(* messages *)
1.89 -
1.90 -fun pgml area content =
1.91 - Pgml.Pgml {version = NONE, systemid = NONE, area = SOME area, content = content};
1.92 -
1.93 -fun message_content default_area s =
1.94 - let
1.95 - val body = YXML.parse_body s;
1.96 - val area =
1.97 - (case body of
1.98 - [XML.Elem ((name, _), _)] =>
1.99 - if name = Markup.stateN then PgipTypes.Display else default_area
1.100 - | _ => default_area);
1.101 - in Pgml.pgml_to_xml (pgml area (maps pgml_terms body)) end;
1.102 -
1.103 -
1.104 -fun normalmsg area s = issue_pgip
1.105 - (Normalresponse {content = [message_content area s]});
1.106 -
1.107 -fun errormsg area fatality s = issue_pgip
1.108 - (Errorresponse {fatality = fatality, location = NONE, content = [message_content area s]});
1.109 -
1.110 -(*error responses with useful locations*)
1.111 -fun error_with_pos area fatality pos s = issue_pgip
1.112 - (Errorresponse {
1.113 - fatality = fatality,
1.114 - location = SOME (PgipIsabelle.location_of_position pos),
1.115 - content = [message_content area s]});
1.116 -
1.117 -fun panic s = (errormsg Message Panic ("## SYSTEM EXIT ##\n" ^ s); exit 1);
1.118 -fun nonfatal_error s = errormsg Message Nonfatal s;
1.119 -fun log_msg s = errormsg Message Log s;
1.120 -
1.121 -(* NB: all of standard functions print strings terminated with new lines, but we don't
1.122 - add new lines explicitly in PGIP: they are left implicit. It means that PGIP messages
1.123 - can't be written without newlines. *)
1.124 -fun setup_messages () =
1.125 - (Output.Private_Hooks.writeln_fn := (fn s => normalmsg Message s);
1.126 - Output.Private_Hooks.status_fn := (fn _ => ());
1.127 - Output.Private_Hooks.report_fn := (fn _ => ());
1.128 - Output.Private_Hooks.urgent_message_fn := (fn s => normalmsg Status s);
1.129 - Output.Private_Hooks.tracing_fn := (fn s => normalmsg Tracing s);
1.130 - Output.Private_Hooks.warning_fn := (fn s => errormsg Message Warning s);
1.131 - Output.Private_Hooks.error_fn := (fn (_, s) => errormsg Message Fatal s));
1.132 -
1.133 -
1.134 -(* immediate messages *)
1.135 -
1.136 -fun tell_clear_goals () =
1.137 - issue_pgip (Normalresponse { content = [Pgml.pgml_to_xml (pgml Display [])] })
1.138 -fun tell_clear_response () =
1.139 - issue_pgip (Normalresponse { content = [Pgml.pgml_to_xml (pgml Message [])] })
1.140 -
1.141 -fun tell_file_loaded completed path =
1.142 - issue_pgip (Informfileloaded {url=PgipTypes.pgipurl_of_path path,
1.143 - completed=completed})
1.144 -fun tell_file_outdated completed path =
1.145 - issue_pgip (Informfileoutdated {url=PgipTypes.pgipurl_of_path path,
1.146 - completed=completed})
1.147 -fun tell_file_retracted completed path =
1.148 - issue_pgip (Informfileretracted {url=PgipTypes.pgipurl_of_path path,
1.149 - completed=completed})
1.150 -
1.151 -
1.152 -(* theory loader actions *)
1.153 -
1.154 -local
1.155 - (* da: TODO: PGIP has a completed flag so the prover can indicate to the
1.156 - interface which files are busy performing a particular action.
1.157 - To make use of this we need to adjust the hook in thy_info.ML
1.158 - (may actually be difficult to tell the interface *which* action is in
1.159 - progress, but we could add a generic "Lock" action which uses
1.160 - informfileloaded: the broker/UI should not infer too much from incomplete
1.161 - operations).
1.162 - *)
1.163 -fun trace_action action name =
1.164 - if action = Thy_Info.Update then
1.165 - List.app (tell_file_loaded true) (Thy_Info.loaded_files name)
1.166 - else if action = Thy_Info.Remove then
1.167 - List.app (tell_file_retracted true) (Thy_Info.loaded_files name)
1.168 - else ()
1.169 -
1.170 -
1.171 -in
1.172 - fun setup_thy_loader () = Thy_Info.add_hook trace_action;
1.173 - fun sync_thy_loader () = List.app (trace_action Thy_Info.Update) (Thy_Info.get_names ());
1.174 -end;
1.175 -
1.176 -
1.177 -(* get informed about files *)
1.178 -
1.179 -val thy_name = Path.implode o #1 o Path.split_ext o Path.base;
1.180 -
1.181 -val inform_file_retracted = Thy_Info.kill_thy o thy_name;
1.182 -
1.183 -fun inform_file_processed path state =
1.184 - let val name = thy_name path in
1.185 - if Toplevel.is_toplevel state then
1.186 - Thy_Info.register_thy (Toplevel.end_theory Position.none state)
1.187 - handle ERROR msg =>
1.188 - (warning (cat_lines [msg, "Failed to register theory: " ^ quote name]);
1.189 - tell_file_retracted true (Path.base path))
1.190 - else raise Toplevel.UNDEF
1.191 - end;
1.192 -
1.193 -
1.194 -(* restart top-level loop (keeps most state information) *)
1.195 -
1.196 -val welcome = Output.urgent_message o Session.welcome;
1.197 -
1.198 -fun restart () =
1.199 - (sync_thy_loader ();
1.200 - tell_clear_goals ();
1.201 - tell_clear_response ();
1.202 - Isar.init ();
1.203 - welcome ());
1.204 -
1.205 -
1.206 (* theorem dependencies *)
1.207
1.208 local
1.209 @@ -272,91 +93,6 @@
1.210 end;
1.211
1.212
1.213 -(* theorem dependeny output *)
1.214 -
1.215 -val show_theorem_dependencies = Unsynchronized.ref false;
1.216 -
1.217 -local
1.218 -
1.219 -val spaces_quote = space_implode " " o map quote;
1.220 -
1.221 -fun thm_deps_message (thms, deps) =
1.222 - let
1.223 - val valuethms = XML.Elem (("value", [("name", "thms")]), [XML.Text thms]);
1.224 - val valuedeps = XML.Elem (("value", [("name", "deps")]), [XML.Text deps]);
1.225 - in
1.226 - issue_pgip (Metainforesponse
1.227 - {attrs = [("infotype", "isabelle_theorem_dependencies")],
1.228 - content = [valuethms, valuedeps]})
1.229 - end;
1.230 -
1.231 -in
1.232 -
1.233 -fun setup_present_hook () = Toplevel.add_hook (fn _ => fn state => fn state' =>
1.234 - if ! show_theorem_dependencies andalso
1.235 - can Toplevel.theory_of state andalso Toplevel.is_theory state'
1.236 - then
1.237 - let val (names, deps) = new_thms_deps (Toplevel.theory_of state) (Toplevel.theory_of state') in
1.238 - if null names orelse null deps then ()
1.239 - else thm_deps_message (spaces_quote names, spaces_quote deps)
1.240 - end
1.241 - else ());
1.242 -
1.243 -end;
1.244 -
1.245 -
1.246 -(** lexicalstructure element with keywords (PGIP version of elisp keywords file) **)
1.247 -
1.248 -fun lexicalstructure_keywords () =
1.249 - let val (keywords, commands) = Keyword.dest ()
1.250 - fun keyword_elt kind keyword =
1.251 - XML.Elem (("keyword", [("word", keyword), ("category", kind)]), [])
1.252 - in
1.253 - Lexicalstructure
1.254 - {content = map (keyword_elt "minor") keywords @ map (keyword_elt "major") commands}
1.255 - end
1.256 -
1.257 -(* TODO: we can issue a lexicalstructure/keyword when the syntax gets extended dynamically;
1.258 - hooks needed in outer_syntax.ML to do that. *)
1.259 -
1.260 -
1.261 -(* Configuration: GUI config, proverinfo messages *)
1.262 -
1.263 -local
1.264 - val isabellewww = "http://isabelle.in.tum.de/"
1.265 - val staticconfig = "~~/lib/ProofGeneral/pgip_isar.xml"
1.266 - fun orenv v d = case getenv v of "" => d | s => s
1.267 - fun config_file() = orenv "ISABELLE_PGIPCONFIG" staticconfig
1.268 - fun isabelle_www() = orenv "ISABELLE_HOMEPAGE" isabellewww
1.269 -in
1.270 -fun send_pgip_config () =
1.271 - let
1.272 - val path = Path.explode (config_file())
1.273 - val ex = File.exists path
1.274 -
1.275 - val wwwpage =
1.276 - (Url.explode (isabelle_www()))
1.277 - handle ERROR _ =>
1.278 - (panic ("Error in URL in environment variable ISABELLE_HOMEPAGE.");
1.279 - Url.explode isabellewww)
1.280 -
1.281 - val proverinfo =
1.282 - Proverinfo { name = "Isabelle",
1.283 - version = Distribution.version,
1.284 - instance = Session.name(),
1.285 - descr = "The Isabelle/Isar theorem prover",
1.286 - url = wwwpage,
1.287 - filenameextns = ".thy;" }
1.288 - in
1.289 - if ex then
1.290 - (issue_pgip proverinfo;
1.291 - issue_pgip_rawtext (File.read path);
1.292 - issue_pgip (lexicalstructure_keywords()))
1.293 - else panic ("PGIP configuration file \"" ^ config_file() ^ "\" not found")
1.294 - end;
1.295 -end
1.296 -
1.297 -
1.298 (* Preferences: tweak for PGIP interfaces *)
1.299
1.300 val preferences = Unsynchronized.ref Preferences.pure_preferences;
1.301 @@ -369,622 +105,8 @@
1.302 SOME {set, ...} => set value
1.303 | NONE => error ("Unknown prover preference: " ^ quote pref));
1.304
1.305 -fun setup_preferences_tweak () =
1.306 - CRITICAL (fn () => Unsynchronized.change preferences
1.307 - (Preferences.set_default ("show-question-marks", "false") #>
1.308 - Preferences.remove "show-question-marks" #> (* we use markup, not ?s *)
1.309 - Preferences.remove "theorem-dependencies" #> (* set internally *)
1.310 - Preferences.remove "full-proofs")); (* set internally *)
1.311
1.312 -
1.313 -
1.314 -(* Sending commands to Isar *)
1.315 -
1.316 -fun isarcmd s = Isar.>>> (Outer_Syntax.parse Position.none s);
1.317 -
1.318 -(* TODO:
1.319 - - apply a command given a transition function;
1.320 - - fix position from path of currently open file [line numbers risk garbling though].
1.321 -*)
1.322 -
1.323 -(* load an arbitrary file (must be .thy or .ML) *)
1.324 -
1.325 -fun use_thy_or_ml_file file =
1.326 - let
1.327 - val (path,extn) = Path.split_ext (Path.explode file)
1.328 - in
1.329 - case extn of
1.330 - "" => isarcmd ("use_thy " ^ quote (Path.implode path))
1.331 - | "thy" => isarcmd ("use_thy " ^ quote (Path.implode path))
1.332 - | "ML" => isarcmd ("use " ^ quote file)
1.333 - | other => error ("Don't know how to read a file with extension " ^ quote other)
1.334 - end
1.335 -
1.336 -
1.337 -(******* PGIP actions *******)
1.338 -
1.339 -
1.340 -(* Responses to each of the PGIP input commands.
1.341 - These are programmed uniformly for extensibility. *)
1.342 -
1.343 -fun askpgip (Askpgip _) =
1.344 - (issue_pgip
1.345 - (Usespgip { version = PgipIsabelle.isabelle_pgip_version_supported,
1.346 - pgipelems = PgipIsabelle.accepted_inputs });
1.347 - send_pgip_config())
1.348 -
1.349 -fun askpgml (Askpgml _) =
1.350 - issue_pgip
1.351 - (Usespgml { version = PgipIsabelle.isabelle_pgml_version_supported })
1.352 -
1.353 -fun askprefs (Askprefs _) =
1.354 - let
1.355 - fun preference_of {name, descr, default, pgiptype, get, set } =
1.356 - { name = name, descr = SOME descr, default = SOME default,
1.357 - pgiptype = pgiptype }
1.358 - in
1.359 - List.app (fn (prefcat, prefs) =>
1.360 - issue_pgip (Hasprefs {prefcategory=SOME prefcat,
1.361 - prefs=map preference_of prefs}))
1.362 - (!preferences)
1.363 - end
1.364 -
1.365 -fun askconfig (Askconfig _) = () (* TODO: add config response *)
1.366 -
1.367 -local
1.368 - fun lookuppref pref =
1.369 - case AList.lookup (op =)
1.370 - (map (fn p => (#name p,p))
1.371 - (maps snd (!preferences))) pref of
1.372 - NONE => error ("Unknown prover preference: " ^ quote pref)
1.373 - | SOME p => p
1.374 -in
1.375 -fun setpref (Setpref vs) =
1.376 - let
1.377 - val name = #name vs
1.378 - val value = #value vs
1.379 - val set = #set (lookuppref name)
1.380 - in
1.381 - set value
1.382 - end
1.383 -
1.384 -fun getpref (Getpref vs) =
1.385 - let
1.386 - val name = #name vs
1.387 - val get = #get (lookuppref name)
1.388 - in
1.389 - issue_pgip (Prefval {name=name, value=get ()})
1.390 - end
1.391 -end
1.392 -
1.393 -fun proverinit _ = restart ()
1.394 -
1.395 -fun proverexit _ = isarcmd "quit"
1.396 -
1.397 -fun set_proverflag_quiet b =
1.398 - isarcmd (if b then "disable_pr" else "enable_pr")
1.399 -
1.400 -fun set_proverflag_pgmlsymbols b =
1.401 - (pgmlsymbols_flag := b;
1.402 - NAMED_CRITICAL "print_mode" (fn () =>
1.403 - Unsynchronized.change print_mode
1.404 - (fn mode =>
1.405 - remove (op =) Symbol.xsymbolsN mode @ (if b then [Symbol.xsymbolsN] else []))))
1.406 -
1.407 -fun set_proverflag_thmdeps b =
1.408 - (show_theorem_dependencies := b;
1.409 - Proofterm.proofs := (if b then 1 else 2))
1.410 -
1.411 -fun setproverflag (Setproverflag vs) =
1.412 - let
1.413 - val flagname = #flagname vs
1.414 - val value = #value vs
1.415 - in
1.416 - (case flagname of
1.417 - "quiet" => set_proverflag_quiet value
1.418 - | "pgmlsymbols" => set_proverflag_pgmlsymbols value
1.419 - | "metainfo:thmdeps" => set_proverflag_thmdeps value
1.420 - | _ => log_msg ("Unrecognised prover control flag: " ^
1.421 - (quote flagname) ^ " ignored."))
1.422 - end
1.423 -
1.424 -
1.425 -fun dostep (Dostep vs) =
1.426 - let
1.427 - val text = #text vs
1.428 - in
1.429 - isarcmd text
1.430 - end
1.431 -
1.432 -fun undostep (Undostep vs) =
1.433 - let
1.434 - val times = #times vs
1.435 - in
1.436 - isarcmd ("undos_proof " ^ string_of_int times)
1.437 - end
1.438 -
1.439 -fun redostep _ = raise Fail "redo unavailable"
1.440 -
1.441 -fun abortgoal _ = isarcmd "kill" (* was: ProofGeneral.kill_proof *)
1.442 -
1.443 -
1.444 -(*** PGIP identifier tables ***)
1.445 -
1.446 -(* TODO: these ones should be triggered by hooks after a
1.447 - declaration addition/removal, to be sent automatically. *)
1.448 -
1.449 -fun addids t = issue_pgip (Addids {idtables = [t]})
1.450 -fun delids t = issue_pgip (Delids {idtables = [t]})
1.451 -
1.452 -
1.453 -local
1.454 -
1.455 -fun theory_facts thy =
1.456 - (map Global_Theory.facts_of (Theory.parents_of thy), Global_Theory.facts_of thy);
1.457 -
1.458 -fun thms_of_thy name =
1.459 - let val thy = Thy_Info.get_theory name
1.460 - in map fst (theory_facts thy |-> Facts.extern_static (Proof_Context.init_global thy)) end;
1.461 -
1.462 -fun qualified_thms_of_thy name =
1.463 - map fst (theory_facts (Thy_Info.get_theory name) |-> Facts.dest_static);
1.464 -
1.465 -in
1.466 -
1.467 -fun askids (Askids vs) =
1.468 - let
1.469 - val url = #url vs (* ask for identifiers within a file *)
1.470 - val thyname = #thyname vs (* ask for identifiers within a theory *)
1.471 - val objtype = #objtype vs (* ask for identifiers of a particular type *)
1.472 -
1.473 - fun idtable ty ctx ids = {objtype=ty,context=ctx,ids=ids}
1.474 -
1.475 - fun setids t = issue_pgip (Setids {idtables = [t]})
1.476 -
1.477 - (* fake one-level nested "subtheories" by picking apart names. *)
1.478 - val immed_thms_of_thy = filter_out Long_Name.is_qualified o thms_of_thy
1.479 - fun thy_prefix s = case Long_Name.explode s of
1.480 - x::_::_ => SOME x (* String.find? *)
1.481 - | _ => NONE
1.482 - fun subthys_of_thy s =
1.483 - List.foldl (fn (NONE,xs) => xs | (SOME x,xs) => insert op= x xs) []
1.484 - (map thy_prefix (thms_of_thy s))
1.485 - fun subthms_of_thy thy =
1.486 - (case thy_prefix thy of
1.487 - NONE => immed_thms_of_thy thy
1.488 - | SOME prf => filter (String.isPrefix (unprefix (prf ^ Long_Name.separator) thy))
1.489 - (thms_of_thy prf))
1.490 - in
1.491 - case (thyname,objtype) of
1.492 - (NONE, NONE) =>
1.493 - setids (idtable ObjFile NONE (Thy_Info.get_names())) (*FIXME: uris*)
1.494 - | (NONE, SOME ObjFile) =>
1.495 - setids (idtable ObjFile NONE (Thy_Info.get_names())) (*FIXME: uris*)
1.496 - | (SOME fi, SOME ObjFile) =>
1.497 - setids (idtable ObjTheory (SOME fi) [fi]) (* TODO: check exists *)
1.498 - | (NONE, SOME ObjTheory) =>
1.499 - setids (idtable ObjTheory NONE (Thy_Info.get_names()))
1.500 - | (SOME thy, SOME ObjTheory) =>
1.501 - setids (idtable ObjTheory (SOME thy) (subthys_of_thy thy))
1.502 - | (SOME thy, SOME ObjTheorem) =>
1.503 - setids (idtable ObjTheorem (SOME thy) (subthms_of_thy thy))
1.504 - | (NONE, SOME ObjTheorem) =>
1.505 - (* A large query, but not unreasonable. ~5000 results for HOL.*)
1.506 - (* Several setids should be allowed, but Eclipse code is currently broken:
1.507 - List.app (fn thy => setids (idtable ObjTheorem (SOME thy) (subthms_of_thy thy)))
1.508 - (Thy_Info.get_names()) *)
1.509 - setids (idtable ObjTheorem NONE (* this one gives ~7000 for HOL *)
1.510 - (maps qualified_thms_of_thy (Thy_Info.get_names())))
1.511 - | _ => warning ("askids: ignored argument combination")
1.512 - end
1.513 -
1.514 -end;
1.515 -
1.516 -fun askrefs (Askrefs vs) =
1.517 - let
1.518 - val url = #url vs (* ask for references of a file (i.e. immediate pre-requisites) *)
1.519 - val thyname = #thyname vs (* ask for references of a theory (other theories) *)
1.520 - val objtype = #objtype vs (* ask for references of a particular type... *)
1.521 - val name = #name vs (* ... with this name *)
1.522 -
1.523 - fun idtable ty ctx ids = {objtype=ty,context=ctx,ids=ids}
1.524 -
1.525 - val thy_name = Path.implode o #1 o Path.split_ext o Path.base
1.526 -
1.527 - fun filerefs f =
1.528 - let val thy = thy_name f
1.529 - in
1.530 - issue_pgip (Setrefs {url=url, thyname=NONE, objtype=SOME PgipTypes.ObjFile,
1.531 - name=NONE, idtables=[], fileurls=[]})
1.532 - end
1.533 -
1.534 - fun thyrefs thy =
1.535 - let val thyrefs = map #1 (#imports (Thy_Load.check_thy Path.current thy))
1.536 - in
1.537 - issue_pgip (Setrefs {url=url, thyname=thyname, objtype=SOME PgipTypes.ObjTheory,
1.538 - name=NONE, idtables=[{context=NONE, objtype=PgipTypes.ObjTheory,
1.539 - ids=thyrefs}], fileurls=[]})
1.540 - end
1.541 -
1.542 - fun thmrefs thmname =
1.543 - let
1.544 - (* TODO: interim: this is probably not right.
1.545 - What we want is mapping onto simple PGIP name/context model. *)
1.546 - val ctx = Toplevel.context_of (Isar.state ()) (* NB: raises UNDEF *)
1.547 - val thy = Proof_Context.theory_of ctx
1.548 - val ths = [Global_Theory.get_thm thy thmname]
1.549 - val deps = #2 (thms_deps ths);
1.550 - in
1.551 - if null deps then ()
1.552 - else issue_pgip (Setrefs {url=url, thyname=thyname, name=name,
1.553 - objtype=SOME PgipTypes.ObjTheorem,
1.554 - idtables=[{context=NONE, objtype=PgipTypes.ObjTheorem,
1.555 - ids=deps}], fileurls=[]})
1.556 - end
1.557 - in
1.558 - case (url,thyname,objtype,name) of
1.559 - (SOME file, NONE, _, _) => filerefs file
1.560 - | (_,SOME thy,_,_) => thyrefs thy
1.561 - | (_,_,SOME PgipTypes.ObjTheorem,SOME thmname) => thmrefs thmname
1.562 - | _ => error ("Unimplemented/invalid case of <askrefs>")
1.563 - end
1.564 -
1.565 -
1.566 -
1.567 -fun showid (Showid vs) =
1.568 - let
1.569 - val thyname = #thyname vs
1.570 - val objtype = #objtype vs
1.571 - val name = #name vs
1.572 -
1.573 - val topthy = Toplevel.theory_of o Isar.state
1.574 -
1.575 - fun splitthy id =
1.576 - let val comps = Long_Name.explode id
1.577 - in case comps of
1.578 - (thy::(rest as _::_)) => (Thy_Info.get_theory thy, Long_Name.implode rest)
1.579 - | [plainid] => (topthy(),plainid)
1.580 - | _ => raise Toplevel.UNDEF (* assert false *)
1.581 - end
1.582 -
1.583 -
1.584 - fun idvalue strings =
1.585 - issue_pgip (Idvalue { thyname=thyname, objtype=objtype, name=name,
1.586 - text=[XML.Elem (("pgml", []), maps YXML.parse_body strings)] })
1.587 -
1.588 - fun strings_of_thm (thy, name) =
1.589 - map (Display.string_of_thm_global thy) (Global_Theory.get_thms thy name)
1.590 -
1.591 - val string_of_thy = Pretty.string_of o Proof_Display.pretty_full_theory false
1.592 - in
1.593 - case (thyname, objtype) of
1.594 - (_, ObjTheory) => idvalue [string_of_thy (Thy_Info.get_theory name)]
1.595 - | (SOME thy, ObjTheorem) => idvalue (strings_of_thm (Thy_Info.get_theory thy, name))
1.596 - | (NONE, ObjTheorem) => idvalue (strings_of_thm (splitthy name))
1.597 - | (_, ot) => error ("Cannot show objects of type "^(PgipTypes.name_of_objtype ot))
1.598 - end
1.599 -
1.600 -(*** Inspecting state ***)
1.601 -
1.602 -(* The file which is currently being processed interactively.
1.603 - In the pre-PGIP code, this was informed to Isabelle and the theory loader
1.604 - on completion, but that allows for circularity in case we read
1.605 - ourselves. So PGIP opens the filename at the start of a script.
1.606 - We ought to prevent problems by modifying the theory loader to know
1.607 - about this special status, but for now we just keep a local reference.
1.608 -*)
1.609 -
1.610 -val currently_open_file = Unsynchronized.ref (NONE : pgipurl option)
1.611 -
1.612 -fun get_currently_open_file () = ! currently_open_file;
1.613 -
1.614 -fun askguise _ =
1.615 - (* The "guise" is the PGIP abstraction of the prover's state.
1.616 - The <informguise> message is merely used for consistency checking. *)
1.617 - let
1.618 - val openfile = !currently_open_file
1.619 -
1.620 - val topthy = Toplevel.theory_of o Isar.state
1.621 - val topthy_name = Context.theory_name o topthy
1.622 -
1.623 - val opentheory = SOME (topthy_name()) handle Toplevel.UNDEF => NONE
1.624 -
1.625 - fun topproofpos () = try Toplevel.proof_position_of (Isar.state ());
1.626 - val openproofpos = topproofpos()
1.627 - in
1.628 - issue_pgip (Informguise { file = openfile,
1.629 - theory = opentheory,
1.630 - (* would be nice to get thm name... *)
1.631 - theorem = NONE,
1.632 - proofpos = openproofpos })
1.633 - end
1.634 -
1.635 -fun parsescript (Parsescript vs) =
1.636 - let
1.637 - val text = #text vs
1.638 - val systemdata = #systemdata vs
1.639 - val location = #location vs (* TODO: extract position *)
1.640 -
1.641 - val doc = PgipParser.pgip_parser Position.none text
1.642 -
1.643 - val sysattrs = PgipTypes.opt_attr "systemdata" systemdata
1.644 - val locattrs = PgipTypes.attrs_of_location location
1.645 - in
1.646 - issue_pgip (Parseresult { attrs= sysattrs@locattrs,
1.647 - doc = doc,
1.648 - errs = [] })
1.649 - end
1.650 -
1.651 -fun showproofstate _ = isarcmd "pr"
1.652 -
1.653 -fun showctxt _ = isarcmd "print_context"
1.654 -
1.655 -fun searchtheorems (Searchtheorems vs) =
1.656 - let
1.657 - val arg = #arg vs
1.658 - in
1.659 - isarcmd ("find_theorems " ^ arg)
1.660 - end
1.661 -
1.662 -fun setlinewidth (Setlinewidth vs) =
1.663 - let
1.664 - val width = #width vs
1.665 - in
1.666 - isarcmd ("pretty_setmargin " ^ string_of_int width) (* FIXME: conversion back/forth! *)
1.667 - end
1.668 -
1.669 -fun viewdoc (Viewdoc vs) =
1.670 - let
1.671 - val arg = #arg vs
1.672 - in
1.673 - isarcmd ("print_" ^ arg) (* FIXME: isabelle doc?. Return URLs, maybe? *)
1.674 - end
1.675 -
1.676 -(*** Theory ***)
1.677 -
1.678 -fun doitem (Doitem vs) =
1.679 - let
1.680 - val text = #text vs
1.681 - in
1.682 - isarcmd text
1.683 - end
1.684 -
1.685 -fun undoitem _ =
1.686 - isarcmd "undo"
1.687 -
1.688 -fun redoitem _ =
1.689 - isarcmd "redo"
1.690 -
1.691 -fun aborttheory _ =
1.692 - isarcmd "kill" (* was: "init_toplevel" *)
1.693 -
1.694 -fun retracttheory (Retracttheory vs) =
1.695 - let
1.696 - val thyname = #thyname vs
1.697 - in
1.698 - isarcmd ("kill_thy " ^ quote thyname)
1.699 - end
1.700 -
1.701 -
1.702 -(*** Files ***)
1.703 -
1.704 -fun changecwd (Changecwd {url, ...}) =
1.705 - Thy_Load.set_master_path (PgipTypes.path_of_pgipurl url)
1.706 -
1.707 -fun openfile (Openfile vs) =
1.708 - let
1.709 - val url = #url vs
1.710 - val filepath = PgipTypes.path_of_pgipurl url
1.711 - val filedir = Path.dir filepath
1.712 - val thy_name = Path.implode o #1 o Path.split_ext o Path.base
1.713 - val openfile_retract = Thy_Info.kill_thy o thy_name;
1.714 - in
1.715 - case !currently_open_file of
1.716 - SOME f => raise PGIP ("<openfile> when a file is already open!\nCurrently open file: " ^
1.717 - PgipTypes.string_of_pgipurl url)
1.718 - | NONE => (openfile_retract filepath;
1.719 - Thy_Load.set_master_path filedir;
1.720 - Output.urgent_message ("Working in file: " ^ PgipTypes.string_of_pgipurl url);
1.721 - currently_open_file := SOME url)
1.722 - end
1.723 -
1.724 -fun closefile _ =
1.725 - case !currently_open_file of
1.726 - SOME f => (inform_file_processed f (Isar.state ());
1.727 - Output.urgent_message
1.728 - ("Finished working in file: " ^ PgipTypes.string_of_pgipurl f);
1.729 - currently_open_file := NONE)
1.730 - | NONE => raise PGIP ("<closefile> when no file is open!")
1.731 -
1.732 -fun loadfile (Loadfile vs) =
1.733 - let
1.734 - val url = #url vs
1.735 - in
1.736 - (* da: this doesn't seem to cause a problem, batch loading uses
1.737 - a different state context. Of course confusion is still possible,
1.738 - e.g. file loaded depends on open file which is not yet saved. *)
1.739 - (* case !currently_open_file of
1.740 - SOME f => raise PGIP ("<loadfile> when a file is open!\nCurrently open file: " ^
1.741 - PgipTypes.string_of_pgipurl url)
1.742 - | NONE => *)
1.743 - use_thy_or_ml_file (File.platform_path url)
1.744 - end
1.745 -
1.746 -fun abortfile _ =
1.747 - case !currently_open_file of
1.748 - SOME f => (isarcmd "init_toplevel";
1.749 - Output.urgent_message ("Aborted working in file: " ^
1.750 - PgipTypes.string_of_pgipurl f);
1.751 - currently_open_file := NONE)
1.752 - | NONE => raise PGIP ("<abortfile> when no file is open!")
1.753 -
1.754 -fun retractfile (Retractfile vs) =
1.755 - let
1.756 - val url = #url vs
1.757 - in
1.758 - case !currently_open_file of
1.759 - SOME f => raise PGIP ("<retractfile> when a file is open!")
1.760 - | NONE => (Output.urgent_message ("Retracting file: " ^ PgipTypes.string_of_pgipurl url);
1.761 - (* TODO: next should be in thy loader, here just for testing *)
1.762 - let
1.763 - val name = thy_name url
1.764 - in List.app (tell_file_retracted false) (Thy_Info.loaded_files name) end;
1.765 - inform_file_retracted url)
1.766 - end
1.767 -
1.768 -
1.769 -(*** System ***)
1.770 -
1.771 -fun systemcmd (Systemcmd vs) =
1.772 - let
1.773 - val arg = #arg vs
1.774 - in
1.775 - isarcmd arg
1.776 - end
1.777 -
1.778 -exception PGIP_QUIT;
1.779 -fun quitpgip _ = raise PGIP_QUIT
1.780 -
1.781 -fun process_input inp = case inp
1.782 - of PgipInput.Askpgip _ => askpgip inp
1.783 - | PgipInput.Askpgml _ => askpgml inp
1.784 - | PgipInput.Askprefs _ => askprefs inp
1.785 - | PgipInput.Askconfig _ => askconfig inp
1.786 - | PgipInput.Getpref _ => getpref inp
1.787 - | PgipInput.Setpref _ => setpref inp
1.788 - | PgipInput.Proverinit _ => proverinit inp
1.789 - | PgipInput.Proverexit _ => proverexit inp
1.790 - | PgipInput.Setproverflag _ => setproverflag inp
1.791 - | PgipInput.Dostep _ => dostep inp
1.792 - | PgipInput.Undostep _ => undostep inp
1.793 - | PgipInput.Redostep _ => redostep inp
1.794 - | PgipInput.Forget _ => error "<forget> not implemented by Isabelle"
1.795 - | PgipInput.Restoregoal _ => error "<restoregoal> not implemented by Isabelle"
1.796 - | PgipInput.Abortgoal _ => abortgoal inp
1.797 - | PgipInput.Askids _ => askids inp
1.798 - | PgipInput.Askrefs _ => askrefs inp
1.799 - | PgipInput.Showid _ => showid inp
1.800 - | PgipInput.Askguise _ => askguise inp
1.801 - | PgipInput.Parsescript _ => parsescript inp
1.802 - | PgipInput.Showproofstate _ => showproofstate inp
1.803 - | PgipInput.Showctxt _ => showctxt inp
1.804 - | PgipInput.Searchtheorems _ => searchtheorems inp
1.805 - | PgipInput.Setlinewidth _ => setlinewidth inp
1.806 - | PgipInput.Viewdoc _ => viewdoc inp
1.807 - | PgipInput.Doitem _ => doitem inp
1.808 - | PgipInput.Undoitem _ => undoitem inp
1.809 - | PgipInput.Redoitem _ => redoitem inp
1.810 - | PgipInput.Aborttheory _ => aborttheory inp
1.811 - | PgipInput.Retracttheory _ => retracttheory inp
1.812 - | PgipInput.Loadfile _ => loadfile inp
1.813 - | PgipInput.Openfile _ => openfile inp
1.814 - | PgipInput.Closefile _ => closefile inp
1.815 - | PgipInput.Abortfile _ => abortfile inp
1.816 - | PgipInput.Retractfile _ => retractfile inp
1.817 - | PgipInput.Changecwd _ => changecwd inp
1.818 - | PgipInput.Systemcmd _ => systemcmd inp
1.819 - | PgipInput.Quitpgip _ => quitpgip inp
1.820 -
1.821 -
1.822 -fun process_pgip_element pgipxml =
1.823 - case pgipxml of
1.824 - xml as (XML.Elem elem) =>
1.825 - (case PgipInput.input elem of
1.826 - NONE => warning ("Unrecognized PGIP command, ignored: \n" ^
1.827 - (XML.string_of xml))
1.828 - | SOME inp => (process_input inp)) (* errors later; packet discarded *)
1.829 - | XML.Text t => ignored_text_warning t
1.830 -and ignored_text_warning t =
1.831 - if size (Symbol.strip_blanks t) > 0 then
1.832 - warning ("Ignored text in PGIP packet: \n" ^ t)
1.833 - else ()
1.834 -
1.835 -fun process_pgip_tree xml =
1.836 - (pgip_refid := NONE;
1.837 - pgip_refseq := NONE;
1.838 - (case xml of
1.839 - XML.Elem (("pgip", attrs), pgips) =>
1.840 - (let
1.841 - val class = PgipTypes.get_attr "class" attrs
1.842 - val dest = PgipTypes.get_attr_opt "destid" attrs
1.843 - val seq = PgipTypes.read_pgipnat (PgipTypes.get_attr "seq" attrs)
1.844 - (* Respond to prover broadcasts, or messages for us. Ignore rest *)
1.845 - val processit =
1.846 - case dest of
1.847 - NONE => class = "pa"
1.848 - | SOME id => matching_pgip_id id
1.849 - in if processit then
1.850 - (pgip_refid := PgipTypes.get_attr_opt "id" attrs;
1.851 - pgip_refseq := SOME seq;
1.852 - List.app process_pgip_element pgips;
1.853 - (* return true to indicate <ready/> *)
1.854 - true)
1.855 - else
1.856 - (* no response to ignored messages. *)
1.857 - false
1.858 - end)
1.859 - | _ => raise PGIP "Invalid PGIP packet received")
1.860 - handle PGIP msg =>
1.861 - (Output.error_msg ((msg ^ "\nPGIP error occurred in XML text below:\n") ^
1.862 - (XML.string_of xml));
1.863 - true))
1.864 -
1.865 -(* External input *)
1.866 -
1.867 -val process_pgip_plain = K () o process_pgip_tree o XML.parse
1.868 -
1.869 -(* PGIP loop: process PGIP input only *)
1.870 -
1.871 -local
1.872 -
1.873 -exception XML_PARSE
1.874 -
1.875 -fun loop ready src =
1.876 - let
1.877 - val _ = if ready then issue_pgip (Ready ()) else ()
1.878 - val pgipo =
1.879 - (case try Source.get_single src of
1.880 - SOME pgipo => pgipo
1.881 - | NONE => raise XML_PARSE)
1.882 - in
1.883 - case pgipo of
1.884 - NONE => ()
1.885 - | SOME (pgip,src') =>
1.886 - let
1.887 - val ready' = (process_pgip_tree pgip)
1.888 - handle PGIP_QUIT => raise PGIP_QUIT
1.889 - | e => (handler (e,SOME src'); true)
1.890 - in
1.891 - loop ready' src'
1.892 - end
1.893 - end handle e => handler (e,SOME src) (* error in XML parse or Ready issue *)
1.894 -
1.895 -and handler (e,srco) =
1.896 - if Exn.is_interrupt e andalso is_some srco then
1.897 - (Output.error_msg "Interrupt during PGIP processing"; loop true (the srco))
1.898 - else
1.899 - case (e,srco) of
1.900 - (XML_PARSE,SOME src) =>
1.901 - panic "Invalid XML input, aborting" (* TODO: attempt recovery *)
1.902 - | (Toplevel.UNDEF,SOME src) =>
1.903 - (Output.error_msg "No working context defined"; loop true src)
1.904 - | (e,SOME src) =>
1.905 - (Output.error_msg (ML_Compiler.exn_message e); loop true src)
1.906 - | (PGIP_QUIT,_) => ()
1.907 - | (_,NONE) => ()
1.908 -in
1.909 - (* TODO: add socket interface *)
1.910 -
1.911 - val xmlP = XML.parse_comments |-- XML.parse_element >> single
1.912 -
1.913 - val tty_src =
1.914 - Source.set_prompt "" (Source.source Symbol.stopper xmlP NONE (Source.tty TextIO.stdIn))
1.915 -
1.916 - fun pgip_toplevel x = loop true x
1.917 -end
1.918 -
1.919 -
1.920 -(** Out-of-loop PGIP commands (for Emacs hybrid mode) **)
1.921 +(** PGIP/Emacs rudiments **)
1.922
1.923 local
1.924
1.925 @@ -994,7 +116,7 @@
1.926
1.927 fun process_element_emacs (XML.Elem (("askprefs", _), _)) =
1.928 let
1.929 - fun preference_of {name, descr, default, pgiptype, get, set} =
1.930 + fun preference_of {name, descr, default, pgiptype, get = _, set = _} =
1.931 {name = name, descr = SOME descr, default = SOME default, pgiptype = pgiptype};
1.932 in
1.933 ! preferences |> List.app (fn (prefcat, prefs) =>
1.934 @@ -1040,11 +162,7 @@
1.935 val _ =
1.936 Outer_Syntax.improper_command
1.937 (("ProofGeneral.process_pgip", Keyword.control), Position.none) "(internal)"
1.938 - (Parse.text >>
1.939 - (fn str => Toplevel.imperative (fn () =>
1.940 - if print_mode_active proof_general_emacsN
1.941 - then process_pgip_emacs str
1.942 - else process_pgip_plain str)));
1.943 + (Parse.text >> (fn str => Toplevel.imperative (fn () => process_pgip_emacs str)));
1.944
1.945 end;
1.946