Experimental version supporting PGIP, merged with main branch with help from Makarius.
1.1 --- a/src/Pure/proof_general.ML Mon Aug 16 17:56:07 2004 +0200
1.2 +++ b/src/Pure/proof_general.ML Mon Aug 16 18:05:41 2004 +0200
1.3 @@ -2,7 +2,25 @@
1.4 ID: $Id$
1.5 Author: David Aspinall and Markus Wenzel
1.6
1.7 -Isabelle configuration for Proof General (see http://proofgeneral.inf.ed.ac.uk).
1.8 +Isabelle configuration for Proof General (see http://proofgeneral.inf.ed.ac.uk)
1.9 +Includes support for PGIP control language for Isabelle/Isar.
1.10 +
1.11 +===========================================================================
1.12 +NOTE: With this version you will lose support for the Isabelle
1.13 +preferences menu in the currently released version of Proof General (3.5).
1.14 +No other changes should be visible in the Emacs interface.
1.15 +
1.16 +If the loss of preferences is a serious problem, please use a "sticky"
1.17 +check-out of the previous version of this file, version 1.27.
1.18 +
1.19 +A version of Proof General which supports the new PGIP format for
1.20 +preferences will be available shortly.
1.21 +===========================================================================
1.22 +
1.23 +STATUS: this version is an interim experimental version that was
1.24 +used from 07.2003-08.2004 for the development of PGIP 1.X. This will
1.25 +soon be replaced by a version for PGIP 2.X.
1.26 +
1.27 *)
1.28
1.29 signature PROOF_GENERAL =
1.30 @@ -12,7 +30,12 @@
1.31 val try_update_thy_only: string -> unit
1.32 val inform_file_retracted: string -> unit
1.33 val inform_file_processed: string -> unit
1.34 - val options: (string * (string * (string * (unit -> string) * (string -> unit)))) list ref
1.35 + val preferences:
1.36 + (string *
1.37 + (string *
1.38 + (string *
1.39 + (string * (string * (unit -> string)) *
1.40 + (string -> unit)))) list) list ref
1.41 val process_pgip: string -> unit
1.42 val thms_containing: string list -> unit
1.43 val help: unit -> unit
1.44 @@ -21,25 +44,35 @@
1.45 val repeat_undo: int -> unit
1.46 val isa_restart: unit -> unit
1.47 val full_proofs: bool -> unit
1.48 + val isarcmd: string -> unit
1.49 val init: bool -> unit
1.50 + val init_pgip: bool -> unit
1.51 val write_keywords: string -> unit
1.52 end;
1.53
1.54 -structure ProofGeneral: PROOF_GENERAL =
1.55 +structure ProofGeneral : PROOF_GENERAL =
1.56 struct
1.57
1.58 +(* PGIP messaging mode (independent of PGML output) *)
1.59 +
1.60 +val pgip_active = ref false;
1.61 +val pgip_emacs_compatibility_flag = ref false;
1.62 +
1.63 +fun pgip () = (!pgip_active);
1.64 +fun pgip_emacs_compatibility () = (!pgip_emacs_compatibility_flag);
1.65 +
1.66 +
1.67 (* print modes *)
1.68
1.69 -val proof_generalN = "ProofGeneral";
1.70 -val xsymbolsN = "xsymbols";
1.71 -val thm_depsN = "thm_deps";
1.72 +val proof_generalN = "ProofGeneral"; (* token markup (colouring vars, etc.) *)
1.73 +val xsymbolsN = Symbol.xsymbolsN; (* XSymbols symbols *)
1.74 +val pgmlN = "PGML"; (* XML escapes and PGML symbol elements *)
1.75 +val pgmlatomsN = "PGMLatoms"; (* variable kind decorations *)
1.76 +val thm_depsN = "thm_deps"; (* meta-information about theorem deps *)
1.77
1.78 -val pgml_version_supported = "1.0";
1.79 -val pgmlN = "PGML";
1.80 fun pgml () = pgmlN mem_string ! print_mode;
1.81
1.82 -
1.83 -(* text output *)
1.84 +(* text output: print modes for xsymbol and PGML *)
1.85
1.86 local
1.87
1.88 @@ -47,20 +80,34 @@
1.89 | xsym_output s = if Symbol.is_raw s then Symbol.decode_raw s else s;
1.90
1.91 fun xsymbols_output s =
1.92 - if Symbol.chars_only s then Symbol.default_output s
1.93 - else if Output.has_mode xsymbolsN then
1.94 + if xsymbolsN mem_string ! print_mode andalso exists_string (equal "\\") s then
1.95 let val syms = Symbol.explode s
1.96 in (implode (map xsym_output syms), real (Symbol.length syms)) end
1.97 - else Symbol.symbol_output s;
1.98 + else Symbol.default_output s;
1.99
1.100 -fun pgml_output (s, len) =
1.101 - if pgml () then (XML.text s, len)
1.102 - else (s, len);
1.103 +fun pgml_sym s =
1.104 + (case Symbol.decode s of
1.105 + Symbol.Char "\\" => "\\\\"
1.106 + | Symbol.Char s => XML.text s
1.107 + | Symbol.Sym s => XML.element "sym" [("name", s)] []
1.108 + | Symbol.Ctrl s => XML.element "ctrl" [("name", s)] []
1.109 + | Symbol.Raw s => s);
1.110
1.111 -in
1.112 +fun pgml_output str =
1.113 + let val syms = Symbol.explode str
1.114 + in (implode (map pgml_sym syms), real (Symbol.length syms)) end;
1.115
1.116 -fun setup_xsymbols_output () = Output.add_mode proof_generalN
1.117 - (pgml_output o xsymbols_output, Symbol.default_indent, Symbol.encode_raw);
1.118 +in
1.119 +
1.120 +fun setup_xsymbols_output () =
1.121 + Output.add_mode
1.122 + xsymbolsN
1.123 + (xsymbols_output, Symbol.default_indent, Symbol.encode_raw);
1.124 +
1.125 +fun setup_pgml_output () =
1.126 + Output.add_mode
1.127 + pgmlN
1.128 + (pgml_output, Symbol.default_indent, Symbol.encode_raw);
1.129
1.130 end;
1.131
1.132 @@ -81,8 +128,10 @@
1.133 fun xml_atom kind x = XML.element "atom" [("kind", kind)] [XML.text x];
1.134
1.135 fun tagit (kind, bg_tag) x =
1.136 - (if pgml () then xml_atom kind x else bg_tag ^ x ^ end_tag,
1.137 - real (Symbol.length (Symbol.explode x)));
1.138 + (if Output.has_mode pgmlatomsN then
1.139 + xml_atom kind x
1.140 + else bg_tag ^ x ^ end_tag,
1.141 + real (Symbol.length (Symbol.explode x)));
1.142
1.143 fun free_or_skolem x =
1.144 (case try Syntax.dest_skolem x of
1.145 @@ -109,259 +158,184 @@
1.146 in val setup = [Theory.add_tokentrfuns proof_general_trans] end;
1.147
1.148
1.149 +(* assembling PGIP packets *)
1.150 +
1.151 +val pgip_refseq = ref None : string option ref
1.152 +val pgip_refid = ref None : string option ref
1.153 +
1.154 +local
1.155 + val myseq_no = ref 1; (* PGIP packet counter *)
1.156 +
1.157 + val pgip_class = "pg"
1.158 + val pgip_origin = "Isabelle/Isar"
1.159 + val pgip_id = (getenv "HOSTNAME") ^ "/" ^ (getenv "USER") ^ "/" ^
1.160 + (Time.toString(Time.now()))
1.161 + (* FIXME: PPID is empty for me: any way to get process ID? *)
1.162 +
1.163 + fun assemble_pgips pgips =
1.164 + XML.element
1.165 + "pgip"
1.166 + ([("class", pgip_class),
1.167 + ("origin", pgip_origin),
1.168 + ("id", pgip_id)] @
1.169 + (if_none (apsome (single o (pair "refseq")) (!pgip_refseq)) []) @
1.170 + (if_none (apsome (single o (pair "refid")) (!pgip_refid)) []) @
1.171 + [("seq", string_of_int (Library.inc myseq_no))])
1.172 + pgips
1.173 +in
1.174 +
1.175 + fun decorated_output bg en prfx =
1.176 + writeln_default o enclose bg en o prefix_lines prfx;
1.177 +
1.178 + (* FIXME: see Rev 1.48 [PG CVS] for cleaner version of this which can be used
1.179 + for PG 4.0 which processes PGIP without needing special chars. *)
1.180 + fun issue_pgips ps =
1.181 + if pgip_emacs_compatibility() then
1.182 + decorated_output (* add urgent message annotation *)
1.183 + (oct_char "360") (oct_char "361") ""
1.184 + (assemble_pgips ps)
1.185 + else
1.186 + writeln_default (assemble_pgips ps)
1.187 +
1.188 + fun assemble_pgip resp attrs s = assemble_pgips [XML.element resp attrs [s]]
1.189 +
1.190 + fun assemble_pgipe resp attrs = assemble_pgips [XML.element resp attrs []]
1.191 +
1.192 + fun issue_pgip resp attrs = writeln_default o (assemble_pgip resp attrs)
1.193 +
1.194 +(* FIXME: temporarily to support PG 3.4. *)
1.195 + fun issue_pgip_maybe_decorated bg en resp attrs s =
1.196 + if pgip_emacs_compatibility() then
1.197 + (* in PGIP mode, but using escape characters as well. *)
1.198 + writeln_default (enclose bg en (assemble_pgip resp attrs s))
1.199 + else
1.200 + issue_pgip resp attrs s
1.201 +
1.202 + fun issue_pgipe resp attrs = writeln_default (assemble_pgipe resp attrs)
1.203 +
1.204 +end
1.205 +
1.206 (* messages and notification *)
1.207
1.208 +fun message resp attrs bg en prfx s =
1.209 + if pgip() then
1.210 + issue_pgip_maybe_decorated bg en resp attrs (prefix_lines prfx s)
1.211 + else
1.212 + decorated_output bg en prfx s;
1.213 +
1.214 +
1.215 local
1.216 + val display_area = ("area", "display")
1.217 + val message_area = ("area", "message")
1.218 + val tracing_category = ("category", "tracing")
1.219 + val urgent_indication = ("urgent", "y")
1.220 + val nonfatal = ("fatality", "nonfatal")
1.221 + val fatal = ("fatality", "fatal")
1.222 + val panic = ("fatality", "panic")
1.223
1.224 -fun decorated_output bg en prfx =
1.225 - writeln_default o enclose bg en o prefix_lines prfx;
1.226 -
1.227 -fun message kind bg en prfx s =
1.228 - if pgml () then writeln_default (XML.element kind [] [prefix_lines prfx s])
1.229 - else decorated_output bg en prfx s;
1.230 -
1.231 -in
1.232 -
1.233 -val notify = message "notify" (oct_char "360") (oct_char "361") "";
1.234 + val thyname_attr = pair "thyname"
1.235 + val url_attr = pair "url"
1.236 + fun localfile_url_attr path = url_attr ("file:///" ^ path)
1.237 +in
1.238
1.239 fun setup_messages () =
1.240 - (writeln_fn := message "output" "" "" "";
1.241 - priority_fn := message "information" (oct_char "360") (oct_char "361") "";
1.242 - tracing_fn := message "tracing" (oct_char "360" ^ oct_char "375") (oct_char "361") "";
1.243 - warning_fn := message "warning" (oct_char "362") (oct_char "363") "### ";
1.244 - error_fn := message "error" (oct_char "364") (oct_char "365") "*** ");
1.245 + (writeln_fn := message "normalresponse" [message_area] "" "" "";
1.246
1.247 -fun tell_clear_goals () = notify "Proof General, please clear the goals buffer.";
1.248 -fun tell_clear_response () = notify "Proof General, please clear the response buffer.";
1.249 -fun tell_file msg path = notify ("Proof General, " ^ msg ^ " " ^ quote (File.sysify_path path));
1.250 -val tell_unlock = tell_file "you can unlock the file";
1.251 + priority_fn := message "normalresponse" [message_area, urgent_indication]
1.252 + (oct_char "360") (oct_char "361") "";
1.253
1.254 -end;
1.255 + tracing_fn := message "normalresponse" [message_area, tracing_category]
1.256 + (oct_char "360" ^ oct_char "375") (oct_char "361") "";
1.257 +
1.258 + warning_fn := message "errorresponse" [nonfatal]
1.259 + (oct_char "362") (oct_char "363") "### ";
1.260 +
1.261 + error_fn := message "errorresponse" [fatal]
1.262 + (oct_char "364") (oct_char "365") "*** ";
1.263 +
1.264 + panic_fn := message "errorresponse" [panic]
1.265 + (oct_char "364") (oct_char "365") "!!! ")
1.266 +
1.267 +
1.268 +(* accumulate printed output in a single PGIP response *)
1.269 +
1.270 +fun with_displaywrap (elt,attrs) dispfn =
1.271 + let
1.272 + val lines = ref ([] : string list);
1.273 + fun wlgrablines s = (lines:= (s :: (!lines)))
1.274 + in
1.275 + (setmp writeln_fn wlgrablines dispfn ();
1.276 + (* FIXME: cat_lines here inefficient, should use stream output *)
1.277 + issue_pgip elt attrs (cat_lines (!lines)))
1.278 + end
1.279 +
1.280 +val emacs_notify = decorated_output (oct_char "360") (oct_char "361") "";
1.281 +
1.282 +fun tell_clear_goals () =
1.283 + if pgip() then
1.284 + issue_pgipe "cleardisplay" [display_area]
1.285 + else
1.286 + emacs_notify "Proof General, please clear the goals buffer.";
1.287 +
1.288 +fun tell_clear_response () =
1.289 + if pgip() then
1.290 + issue_pgipe "cleardisplay" [message_area]
1.291 + else
1.292 + emacs_notify "Proof General, please clear the response buffer.";
1.293 +
1.294 +fun tell_file_loaded path =
1.295 + if pgip() then
1.296 + issue_pgipe "informtheoryloaded" (* FIXME: get thy name from info here? *)
1.297 + [thyname_attr (XML.text (File.sysify_path path)),
1.298 + localfile_url_attr (XML.text (File.sysify_path path))]
1.299 + else
1.300 + emacs_notify ("Proof General, this file is loaded: "
1.301 + ^ quote (File.sysify_path path));
1.302 +
1.303 +fun tell_file_retracted path =
1.304 + if pgip() then
1.305 + issue_pgipe "informtheoryretracted" (* FIXME: get thy name from info here? *)
1.306 + [thyname_attr (XML.text (File.sysify_path path)),
1.307 + localfile_url_attr (XML.text (File.sysify_path path))]
1.308 + else
1.309 + emacs_notify ("Proof General, you can unlock the file "
1.310 + ^ quote (File.sysify_path path));
1.311
1.312
1.313 (* theory / proof state output *)
1.314
1.315 local
1.316
1.317 -fun tmp_markers f =
1.318 - setmp Display.current_goals_markers (oct_char "366", oct_char "367", "") f ();
1.319 + fun tmp_markers f = setmp Display.current_goals_markers
1.320 + (oct_char "366", oct_char "367", "") f ()
1.321
1.322 -fun statedisplay prts =
1.323 - writeln_default (XML.element "statedisplay" [] [Pretty.string_of (Pretty.chunks prts)]);
1.324 + fun statedisplay prts =
1.325 + issue_pgip "proofstate" []
1.326 + (XML.element "pgml" []
1.327 + [XML.element "statedisplay"
1.328 + []
1.329 + [Output.output (* FIXME: needed? *)
1.330 + (Pretty.output
1.331 + (Pretty.chunks prts))]])
1.332
1.333 -fun print_current_goals n m st =
1.334 - if pgml () then statedisplay (Display.pretty_current_goals n m st)
1.335 - else tmp_markers (fn () => Display.print_current_goals_default n m st);
1.336 -
1.337 -fun print_state b st =
1.338 - if pgml () then statedisplay (Toplevel.pretty_state b st)
1.339 - else tmp_markers (fn () => Toplevel.print_state_default b st);
1.340 -
1.341 + fun print_current_goals n m st =
1.342 + if pgml () then statedisplay (Display.pretty_current_goals n m st)
1.343 + else tmp_markers (fn () => Display.print_current_goals_default n m st)
1.344 +
1.345 + fun print_state b st =
1.346 + if pgml () then statedisplay (Toplevel.pretty_state b st)
1.347 + else tmp_markers (fn () => Toplevel.print_state_default b st)
1.348 in
1.349
1.350 -fun setup_state () =
1.351 - (Display.print_current_goals_fn := print_current_goals;
1.352 - Toplevel.print_state_fn := print_state;
1.353 - Toplevel.prompt_state_fn := (suffix (oct_char "372") o Toplevel.prompt_state_default));
1.354 + fun setup_state () =
1.355 + (Display.print_current_goals_fn := print_current_goals;
1.356 + Toplevel.print_state_fn := print_state;
1.357 + (* FIXME: check next octal char won't appear in pgip? *)
1.358 + Toplevel.prompt_state_fn := (suffix (oct_char "372") o
1.359 + Toplevel.prompt_state_default));
1.360 +end
1.361
1.362 -end;
1.363 -
1.364 -
1.365 -(* theorem dependency output *)
1.366 -
1.367 -local
1.368 -
1.369 -val spaces_quote = space_implode " " o map quote;
1.370 -
1.371 -fun tell_thm_deps ths =
1.372 - conditional (thm_depsN mem_string ! print_mode) (fn () =>
1.373 - let
1.374 - val names = map Thm.name_of_thm ths \ "";
1.375 - val deps = Symtab.keys (foldl (uncurry Proofterm.thms_of_proof)
1.376 - (Symtab.empty, map Thm.proof_of ths)) \ "";
1.377 - in
1.378 - if null names orelse null deps then ()
1.379 - else notify ("Proof General, theorem dependencies of " ^ spaces_quote names ^ " are "
1.380 - ^ spaces_quote deps)
1.381 - end);
1.382 -
1.383 -in
1.384 -
1.385 -fun setup_present_hook () =
1.386 - Present.add_hook (fn _ => fn res => tell_thm_deps (flat (map #2 res)));
1.387 -
1.388 -end;
1.389 -
1.390 -
1.391 -(* theory loader actions *)
1.392 -
1.393 -local
1.394 -
1.395 -fun add_master_files name files =
1.396 - let val masters = [ThyLoad.thy_path name, ThyLoad.ml_path name]
1.397 - in masters @ gen_rems (op = o pairself Path.base) (files, masters) end;
1.398 -
1.399 -fun trace_action action name =
1.400 - if action = ThyInfo.Update then
1.401 - seq (tell_file "this file is loaded:") (ThyInfo.loaded_files name)
1.402 - else if action = ThyInfo.Outdate orelse action = ThyInfo.Remove then
1.403 - seq tell_unlock (add_master_files name (ThyInfo.loaded_files name))
1.404 - else ();
1.405 -
1.406 -in
1.407 - fun setup_thy_loader () = ThyInfo.add_hook trace_action;
1.408 - fun sync_thy_loader () = seq (trace_action ThyInfo.Update) (ThyInfo.names ());
1.409 -end;
1.410 -
1.411 -
1.412 -(* prepare theory context *)
1.413 -
1.414 -val thy_name = Path.pack o #1 o Path.split_ext o Path.base o Path.unpack;
1.415 -val update_thy_only = setmp MetaSimplifier.trace_simp false ThyInfo.update_thy_only;
1.416 -
1.417 -fun which_context () =
1.418 - (case Context.get_context () of
1.419 - Some thy => " Using current (dynamic!) one: " ^
1.420 - (case try PureThy.get_name thy of Some name => quote name | None => "<unnamed>")
1.421 - | None => "");
1.422 -
1.423 -fun try_update_thy_only file =
1.424 - ThyLoad.cond_add_path (Path.dir (Path.unpack file)) (fn () =>
1.425 - let val name = thy_name file in
1.426 - if is_some (ThyLoad.check_file (ThyLoad.thy_path name)) then update_thy_only name
1.427 - else warning ("Unkown theory context of ML file." ^ which_context ())
1.428 - end) ();
1.429 -
1.430 -
1.431 -(* get informed about files *)
1.432 -
1.433 -val inform_file_retracted = ThyInfo.if_known_thy ThyInfo.remove_thy o thy_name;
1.434 -val inform_file_processed = ThyInfo.if_known_thy ThyInfo.touch_child_thys o thy_name;
1.435 -
1.436 -fun proper_inform_file_processed file state =
1.437 - let val name = thy_name file in
1.438 - if Toplevel.is_toplevel state andalso ThyInfo.known_thy name then
1.439 - (ThyInfo.touch_child_thys name;
1.440 - transform_error ThyInfo.pretend_use_thy_only name handle ERROR_MESSAGE msg =>
1.441 - (warning msg; warning ("Failed to register theory: " ^ quote name);
1.442 - tell_unlock (Path.base (Path.unpack file))))
1.443 - else raise Toplevel.UNDEF
1.444 - end;
1.445 -
1.446 -fun vacuous_inform_file_processed file state =
1.447 - (warning ("No theory " ^ quote (thy_name file));
1.448 - tell_unlock (Path.base (Path.unpack file)));
1.449 -
1.450 -
1.451 -(* options *)
1.452 -
1.453 -fun nat_option r = ("nat",
1.454 - (fn () => string_of_int (!r)),
1.455 - (fn s => (case Syntax.read_nat s of
1.456 - None => error "nat_option: illegal value"
1.457 - | Some i => r := i)));
1.458 -
1.459 -fun bool_option r = ("boolean",
1.460 - (fn () => Bool.toString (!r)),
1.461 - (fn "false" => r := false | "true" => r := true
1.462 - | _ => error "bool_option: illegal value"));
1.463 -
1.464 -val proof_option = ("boolean",
1.465 - (fn () => Bool.toString (!proofs >= 2)),
1.466 - (fn "false" => proofs := 1 | "true" => proofs := 2
1.467 - | _ => error "proof_option: illegal value"));
1.468 -
1.469 -val thm_deps_option = ("boolean",
1.470 - (fn () => Bool.toString ("thm_deps" mem !print_mode)),
1.471 - (fn "false" => print_mode := Library.gen_rems (op =) (!print_mode, ["thm_deps"])
1.472 - | "true" => print_mode := (["thm_deps"] @ !print_mode)
1.473 - | _ => error "thm_deps_option: illegal value"));
1.474 -
1.475 -val print_depth_option = ("nat",
1.476 - (fn () => "10"),
1.477 - (fn s => (case Syntax.read_nat s of
1.478 - None => error "print_depth_option: illegal value"
1.479 - | Some i => print_depth i)));
1.480 -
1.481 -val options = ref
1.482 - [("show-types", ("Whether to show types in Isabelle.",
1.483 - bool_option show_types)),
1.484 - ("show-sorts", ("Whether to show sorts in Isabelle.",
1.485 - bool_option show_sorts)),
1.486 - ("show-structs", ("Whether to show implicit structures in Isabelle.",
1.487 - bool_option show_structs)),
1.488 - ("show-consts", ("Whether to show types of consts in Isabelle goals.",
1.489 - bool_option show_consts)),
1.490 - ("long-names", ("Whether to show fully qualified names in Isabelle.",
1.491 - bool_option long_names)),
1.492 - ("show-brackets", ("Whether to show full bracketing in Isabelle.",
1.493 - bool_option show_brackets)),
1.494 - ("eta-contract", ("Whether to print terms eta-contracted in Isabelle.",
1.495 - bool_option Syntax.eta_contract)),
1.496 - ("trace-simplifier", ("Whether to trace the Simplifier in Isabelle.",
1.497 - bool_option trace_simp)),
1.498 - ("trace-rules", ("Whether to trace the standard rules in Isabelle.",
1.499 - bool_option trace_rules)),
1.500 - ("quick-and-dirty", ("Whether to take a few short cuts occasionally.",
1.501 - bool_option quick_and_dirty)),
1.502 - ("full-proofs", ("Whether to record full proof objects internally.",
1.503 - proof_option)),
1.504 - ("trace-unification", ("Whether to output error diagnostics during unification.",
1.505 - bool_option Pattern.trace_unify_fail)),
1.506 - ("show-main-goal", ("Whether to show main goal.",
1.507 - bool_option Proof.show_main_goal)),
1.508 - ("global-timing", ("Whether to enable timing in Isabelle.",
1.509 - bool_option Output.timing)),
1.510 - ("theorem-dependencies", ("Whether to track theorem dependencies within Proof General.",
1.511 - thm_deps_option)),
1.512 - ("goals-limit", ("Setting for maximum number of goals printed in Isabelle.",
1.513 - nat_option goals_limit)),
1.514 - ("prems-limit", ("Setting for maximum number of premises printed in Isabelle/Isar.",
1.515 - nat_option ProofContext.prems_limit)),
1.516 - ("print-depth", ("Setting for the ML print depth in Isabelle.",
1.517 - print_depth_option))];
1.518 -
1.519 -
1.520 -(* sending PGIP commands to the interface *)
1.521 -
1.522 -fun issue_pgip pgips = notify (XML.element "pgip" [] pgips);
1.523 -
1.524 -fun usespgml () =
1.525 - issue_pgip [XML.element "usespgml" [("version", pgml_version_supported)] []];
1.526 -
1.527 -(*NB: the default returned here is actually the current value, so
1.528 - repeated uses of <askprefs> will not work correctly*)
1.529 -fun show_options () = issue_pgip (map
1.530 - (fn (name, (descr, (ty, get, _))) => (XML.element "oldhaspref"
1.531 - [("type", ty), ("descr", descr), ("default", get ())] [name])) (!options));
1.532 -
1.533 -fun set_option name value = (case assoc (!options, name) of
1.534 - None => warning ("Unknown option: " ^ quote name)
1.535 - | Some (_, (_, _, set)) => set value);
1.536 -
1.537 -fun get_option name = (case assoc (!options, name) of
1.538 - None => warning ("Unknown option: " ^ quote name)
1.539 - | Some (_, (_, get, _)) =>
1.540 - issue_pgip [XML.element "prefval" [("name", name)] [get ()]]);
1.541 -
1.542 -
1.543 -(* processing PGIP commands from the interface *)
1.544 -
1.545 -(*FIXME: matching on attributes is a bit too strict here*)
1.546 -
1.547 -fun process_pgip_element pgip = (case pgip of
1.548 - XML.Elem ("askpgml", _, []) => usespgml ()
1.549 - | XML.Elem ("askprefs", _, []) => show_options ()
1.550 - | XML.Elem ("getpref", [("name", name)], []) => get_option name
1.551 - | XML.Elem ("setpref", [("name", name)], [XML.Text value]) =>
1.552 - set_option name value
1.553 - | XML.Elem (e, _, _) => warning ("Unrecognized PGIP command: " ^ e)
1.554 - | XML.Text t => warning ("Unrecognized PGIP command:\n" ^ t));
1.555 -
1.556 -fun process_pgip s = (case XML.tree_of_string s of
1.557 - XML.Elem ("pgip", _, pgips) => seq process_pgip_element pgips
1.558 - | _ => warning ("Invalid PGIP packet received\n" ^ s));
1.559 -
1.560 +end
1.561
1.562 (* misc commands for ProofGeneral/isa *)
1.563
1.564 @@ -381,6 +355,70 @@
1.565 | repeat_undo n = (no_print_goals undo (); repeat_undo (n - 1));
1.566
1.567
1.568 +(* theory loader actions *)
1.569 +
1.570 +local
1.571 +
1.572 +fun add_master_files name files =
1.573 + let val masters = [ThyLoad.thy_path name, ThyLoad.ml_path name]
1.574 + in masters @ gen_rems (op = o pairself Path.base) (files, masters) end;
1.575 +
1.576 +fun trace_action action name =
1.577 + if action = ThyInfo.Update then
1.578 + seq tell_file_loaded (ThyInfo.loaded_files name)
1.579 + else if action = ThyInfo.Outdate orelse action = ThyInfo.Remove then
1.580 + seq tell_file_retracted (add_master_files name (ThyInfo.loaded_files name))
1.581 + else ();
1.582 +
1.583 +in
1.584 + fun setup_thy_loader () = ThyInfo.add_hook trace_action;
1.585 + fun sync_thy_loader () = seq (trace_action ThyInfo.Update) (ThyInfo.names ());
1.586 +end;
1.587 +
1.588 +
1.589 +(* prepare theory context *)
1.590 +
1.591 +val thy_name = Path.pack o #1 o Path.split_ext o Path.base o Path.unpack;
1.592 +val update_thy_only = setmp MetaSimplifier.trace_simp
1.593 + false ThyInfo.update_thy_only;
1.594 +
1.595 +fun which_context () =
1.596 + (case Context.get_context () of
1.597 + Some thy => " Using current (dynamic!) one: " ^
1.598 + (case try PureThy.get_name thy of Some name => quote name | None => "<unnamed>")
1.599 + | None => "");
1.600 +
1.601 +fun try_update_thy_only file =
1.602 + ThyLoad.cond_add_path (Path.dir (Path.unpack file)) (fn () =>
1.603 + let val name = thy_name file in
1.604 + if is_some (ThyLoad.check_file (ThyLoad.thy_path name))
1.605 + then update_thy_only name
1.606 + else warning ("Unkown theory context of ML file." ^ which_context ())
1.607 + end) ();
1.608 +
1.609 +
1.610 +(* get informed about files *)
1.611 +
1.612 +val inform_file_retracted =
1.613 + ThyInfo.if_known_thy ThyInfo.remove_thy o thy_name;
1.614 +val inform_file_processed =
1.615 + ThyInfo.if_known_thy ThyInfo.touch_child_thys o thy_name;
1.616 +
1.617 +fun proper_inform_file_processed file state =
1.618 + let val name = thy_name file in
1.619 + if Toplevel.is_toplevel state andalso ThyInfo.known_thy name then
1.620 + (ThyInfo.touch_child_thys name;
1.621 + transform_error ThyInfo.pretend_use_thy_only name handle ERROR_MESSAGE msg =>
1.622 + (warning msg; warning ("Failed to register theory: " ^ quote name);
1.623 + tell_file_retracted (Path.base (Path.unpack file))))
1.624 + else raise Toplevel.UNDEF
1.625 + end;
1.626 +
1.627 +fun vacuous_inform_file_processed file state =
1.628 + (warning ("No theory " ^ quote (thy_name file));
1.629 + tell_file_retracted (Path.base (Path.unpack file)));
1.630 +
1.631 +
1.632 (* restart top-level loop (keeps most state information) *)
1.633
1.634 local
1.635 @@ -397,16 +435,649 @@
1.636
1.637 end;
1.638
1.639 -
1.640 fun full_proofs true = proofs := 2
1.641 | full_proofs false = proofs := 1;
1.642
1.643
1.644 -(* outer syntax *)
1.645 +(* theorem dependency output *)
1.646 +
1.647 +local
1.648 +
1.649 +val spaces_quote = space_implode " " o map quote;
1.650 +
1.651 +fun thm_deps_message (thms, deps) =
1.652 + if pgip() then
1.653 + issue_pgips
1.654 + [XML.element
1.655 + "metainforesponse" (* FIXME: get thy name from info here? *)
1.656 + [("infotype", "isabelle_theorem_dependencies")]
1.657 + [XML.element "value" [("name", "thms")] [XML.text thms],
1.658 + XML.element "value" [("name", "deps")] [XML.text deps]]]
1.659 + else emacs_notify
1.660 + ("Proof General, theorem dependencies of "
1.661 + ^ thms ^ " are " ^ deps)
1.662 +
1.663 +
1.664 +fun tell_thm_deps ths =
1.665 + conditional (thm_depsN mem_string ! print_mode) (fn () =>
1.666 + let
1.667 + val names = map Thm.name_of_thm ths \ "";
1.668 + val deps = Symtab.keys (foldl (uncurry Proofterm.thms_of_proof)
1.669 + (Symtab.empty, map Thm.proof_of ths)) \ "";
1.670 + in
1.671 + if null names orelse null deps then ()
1.672 + else thm_deps_message (spaces_quote names, spaces_quote deps)
1.673 + end);
1.674 +
1.675 +in
1.676 +
1.677 +fun setup_present_hook () =
1.678 + Present.add_hook (fn _ => fn res => tell_thm_deps (flat (map #2 res)));
1.679 +
1.680 +end;
1.681 +
1.682 +
1.683 +(*** Preferences ***)
1.684 +
1.685 +local
1.686 +val pgipnat = XML.element "pgipint" [("min", "0")] []
1.687 +fun pgipnatmax max = XML.element "pgipint" [("min", "0"),
1.688 + ("max", string_of_int max)] []
1.689 +val pgipbool = XML.element "pgipbool" [] []
1.690 +
1.691 +fun withdefault f = (f(), f)
1.692 +in
1.693 +
1.694 +fun nat_option r = (pgipnat,
1.695 + withdefault (fn () => string_of_int (!r)),
1.696 + (fn s => (case Syntax.read_nat s of
1.697 + None => error "nat_option: illegal value"
1.698 + | Some i => r := i)));
1.699 +
1.700 +fun bool_option r = (pgipbool,
1.701 + withdefault (fn () => Bool.toString (!r)),
1.702 + (fn "false" => r := false | "true" => r := true
1.703 + | _ => error "bool_option: illegal value"));
1.704 +
1.705 +val proof_option = (pgipbool,
1.706 + withdefault (fn () => Bool.toString (!proofs >= 2)),
1.707 + (fn "false" => proofs := 1 | "true" => proofs := 2
1.708 + | _ => error "proof_option: illegal value"));
1.709 +
1.710 +val thm_deps_option = (pgipbool,
1.711 + withdefault (fn () => Bool.toString (Output.has_mode "thm_deps")),
1.712 + (fn "false" => print_mode := ((!print_mode) \ "thm_deps")
1.713 + | "true" => print_mode := ("thm_deps" ins (!print_mode))
1.714 + | _ => error "thm_deps_option: illegal value"));
1.715 +
1.716 +local
1.717 + val pg_print_depth_val = ref 10
1.718 + fun pg_print_depth n = (print_depth n; pg_print_depth_val := n)
1.719 +in
1.720 +val print_depth_option = (pgipnat,
1.721 + withdefault (fn () => string_of_int (!pg_print_depth_val)),
1.722 + (fn s => (case Syntax.read_nat s of
1.723 + None => error "print_depth_option: illegal value"
1.724 + | Some i => pg_print_depth i)))
1.725 +end
1.726 +
1.727 +val preferences = ref
1.728 + [("Display",
1.729 + [("show-types",
1.730 + ("Include types in display of Isabelle terms",
1.731 + bool_option show_types)),
1.732 + ("show-sorts",
1.733 + ("Include sorts in display of Isabelle terms",
1.734 + bool_option show_sorts)),
1.735 + ("show-consts",
1.736 + ("Show types of consts in Isabelle goal display",
1.737 + bool_option show_consts)),
1.738 + ("long-names",
1.739 + ("Show fully qualified names in Isabelle terms", bool_option long_names)),
1.740 + ("show-brackets",
1.741 + ("Show full bracketing in Isabelle terms",
1.742 + bool_option show_brackets)),
1.743 + ("show-main-goal",
1.744 + ("Show main goal in proof state display", bool_option Proof.show_main_goal)),
1.745 + ("eta-contract",
1.746 + ("Print terms eta-contracted",
1.747 + bool_option Syntax.eta_contract))]),
1.748 + ("Advanced Display",
1.749 + [("goals-limit",
1.750 + ("Setting for maximum number of goals printed",
1.751 + nat_option goals_limit)),
1.752 + ("prems-limit",
1.753 + ("Setting for maximum number of premises printed",
1.754 + nat_option ProofContext.prems_limit)),
1.755 + ("print-depth",
1.756 + ("Setting for the ML print depth",
1.757 + print_depth_option))]),
1.758 + ("Tracing",
1.759 + [("trace-simplifier",
1.760 + ("Trace simplification rules.",
1.761 + bool_option trace_simp)),
1.762 + ("trace-rules", ("Trace application of the standard rules",
1.763 + bool_option trace_rules)),
1.764 + ("trace-unification",
1.765 + ("Output error diagnostics during unification",
1.766 + bool_option Pattern.trace_unify_fail)),
1.767 + ("global-timing",
1.768 + ("Whether to enable timing in Isabelle.",
1.769 + bool_option Output.timing))]),
1.770 + ("Proof",
1.771 + [("quick-and-dirty",
1.772 + ("Take a few (interactive-only) short cuts",
1.773 + bool_option quick_and_dirty)),
1.774 + ("full-proofs",
1.775 + ("Record full proof objects internally",
1.776 + proof_option)),
1.777 + ("theorem-dependencies",
1.778 + ("Track theorem dependencies within Proof General",
1.779 + thm_deps_option))])
1.780 + ];
1.781 +end
1.782 +
1.783 +(* Configuration: GUI config, proverinfo messages *)
1.784 +
1.785 +local
1.786 + val config_file = "~~/lib/ProofGeneral/pgip_isar.xml"
1.787 + val name_attr = pair "name"
1.788 + val version_attr = pair "version"
1.789 + val isabelle_www = "http://isabelle.in.tum.de/"
1.790 +in
1.791 +fun send_pgip_config () =
1.792 + let
1.793 + val path = Path.unpack config_file
1.794 + val exists = File.exists path
1.795 + val proverinfo =
1.796 + XML.element "proverinfo"
1.797 + [("name",Session.name()), ("version", version),
1.798 + ("url", isabelle_www)]
1.799 + [XML.element "welcomemsg" [] [XML.text (Session.welcome())],
1.800 + XML.element "helpdoc"
1.801 + (* NB: would be nice to generate/display docs from isatool
1.802 + doc, but that program may not be running on same machine;
1.803 + front end should be responsible for launching viewer, etc. *)
1.804 + [("name", "Isabelle/HOL Tutorial"),
1.805 + ("descr", "A Gentle Introduction to Isabelle/HOL"),
1.806 + ("url", "http://isabelle.in.tum.de/dist/Isabelle2003/doc/tutorial.pdf")]
1.807 + []]
1.808 + in
1.809 + if exists then
1.810 + (issue_pgips [proverinfo]; issue_pgips [File.read path])
1.811 + else panic ("PGIP configuration file " ^ config_file ^ " not found")
1.812 + end;
1.813 +end
1.814 +
1.815 +
1.816 +(* PGIP identifier tables (prover objects). [incomplete] *)
1.817 +
1.818 +local
1.819 + val objtype_thy = "theory"
1.820 + val objtype_thm = "theorem"
1.821 + val objtype_term = "term"
1.822 + val objtype_type = "type"
1.823 +
1.824 + fun xml_idtable ty ctx ids =
1.825 + let
1.826 + fun ctx_attr (Some c)= [("context", c)]
1.827 + | ctx_attr None = []
1.828 + fun xmlid x = XML.element "identifier" [] [XML.text x];
1.829 + in
1.830 + XML.element "idtable" (("objtype", ty)::ctx_attr ctx)
1.831 + (map xmlid ids)
1.832 + end
1.833 +in
1.834 +
1.835 +fun setids t = issue_pgip "setids" [] t
1.836 +fun addids t = issue_pgip "addids" [] t
1.837 +fun delids t = issue_pgip "delids" [] t
1.838 +
1.839 +fun delallids ty = setids (xml_idtable ty None [])
1.840 +
1.841 +fun send_thy_idtable ctx thys = setids (xml_idtable objtype_thy ctx thys)
1.842 +fun clear_thy_idtable () = delallids objtype_thy
1.843 +
1.844 +fun send_thm_idtable ctx thy =
1.845 + addids (xml_idtable objtype_thm ctx (map fst (PureThy.thms_of thy)));
1.846 +
1.847 +fun clear_thm_idtable () = delallids objtype_thm
1.848 +
1.849 +(* fun send_type_idtable thy = TODO, it's a bit low-level messy
1.850 + & maybe not so useful anyway *)
1.851 +
1.852 +end
1.853 +
1.854 +(* Response to interface queries about known objects *)
1.855 +
1.856 +local
1.857 + val topthy = Toplevel.theory_of o Toplevel.get_state
1.858 + val pthm = print_thm oo get_thm
1.859 +
1.860 + fun idvalue tp nm = ("idvalue",[("objtype",tp),("name",nm)])
1.861 +in
1.862 +fun askids (None, Some "theory") = send_thy_idtable None (ThyInfo.names())
1.863 + | askids (None, None) = send_thy_idtable None (ThyInfo.names())
1.864 + (* only theories known in top context *)
1.865 + | askids (Some thy, Some "theory") = send_thy_idtable (Some thy) (ThyInfo.get_preds thy)
1.866 + | askids (Some thy, Some "theorem") = send_thm_idtable (Some thy) (ThyInfo.get_theory thy)
1.867 + | askids (Some thy, None) = (send_thy_idtable (Some thy) (ThyInfo.get_preds thy);
1.868 + send_thm_idtable (Some thy) (ThyInfo.get_theory thy))
1.869 +(* | askids (Some thy, "type") = send_type_idtable (Some thy) (ThyInfo.get_theory thy) *)
1.870 + | askids (_, Nothing) = error "No objects of any type are available here."
1.871 + | askids (_, Some ot) = error ("No objects of type "^(quote ot)^" are available here.")
1.872 +
1.873 +fun showid (_, "theory", n) =
1.874 + with_displaywrap (idvalue "theory" n) (fn ()=>(print_theory (ThyInfo.get_theory n)))
1.875 + | showid (Some thy, "theorem", t) =
1.876 + with_displaywrap (idvalue "theorem" t) (fn ()=>(pthm (ThyInfo.get_theory thy) t))
1.877 + | showid (None, "theorem", t) =
1.878 + with_displaywrap (idvalue "theorem" t) (fn ()=>pthm (topthy()) t)
1.879 + | showid (_, ot, _) = error ("Cannot show objects of type "^ot)
1.880 +
1.881 +(* Return script command to set an identifier to some value *)
1.882 +(* TODO: support object preference setting here *)
1.883 +fun bindid (name, "thm", [XML.Elem ("objval",_,[XML.Text objval])]) =
1.884 + ("lemmas " ^ name ^ " = " ^ objval)
1.885 + | bindid (name, ot, _) = error ("Cannot bind objects of type " ^ ot)
1.886 +
1.887 +end
1.888 +
1.889 +(** Parsing proof scripts without execution **)
1.890 +
1.891 +local
1.892 + (* This is a temporary hack until we have decent parsing of proof scripts *)
1.893 + fun xmle elt = XML.element elt [] []
1.894 + fun xmlc elt str = XML.element elt [] [XML.text str]
1.895 +
1.896 + fun make_opengoal args =
1.897 + (* For now, strictly only args like <lemma foo: "P->Q"> *)
1.898 + let
1.899 + val tstart = find_index_eq "\"" (explode args)
1.900 + val tend = find_index_eq "\"" (drop (tstart, (explode args)))
1.901 + val nend = find_index_eq ":" (explode args)
1.902 + val uptonend = (rev (take (nend-1,explode args)))
1.903 + val nstart = (length uptonend) -
1.904 + (find_index (not o Symbol.is_letter) uptonend)
1.905 + in
1.906 + (XML.element
1.907 + "opengoal"
1.908 + [("thmname", String.substring(args,nstart,nend-nstart))]
1.909 + [XML.text (String.substring(args, tstart+1, tend))])
1.910 + end
1.911 +
1.912 + fun make_theory args =
1.913 + (* For now, strictly only args like <theory Foo=Main:> *)
1.914 + let
1.915 + val argstart = find_index_eq "=" (explode args)
1.916 + val argend = find_index_eq ":" (explode args)
1.917 + val (name1,arg1) = splitAt(argstart, explode args)
1.918 + val namecs = dropwhile (fn c => c mem [" ","\t","\n"]) (rev name1)
1.919 + val nameend = find_index (fn c=> not (Symbol.is_quasi_letter c)) namecs
1.920 + val (namecs',_) = splitAt(nameend, namecs)
1.921 + val name = implode (rev namecs')
1.922 + val (arg2, _) = splitAt(argend-argstart-1, tl arg1)
1.923 + val arg = implode arg2
1.924 + in
1.925 + XML.element "opentheory" [("thyname", name)] [XML.text arg]
1.926 + end
1.927 +in
1.928 +fun xmls_of_transition (name,toks,tr) =
1.929 + let
1.930 + val str = name ^ " " ^ (space_implode " " (map OuterLex.unparse toks))
1.931 + in
1.932 + case name of (* NB: see isar_syn.ML for names of standard commands *)
1.933 + "done" => [xmle "closegoal"]
1.934 + | "sorry" => [xmle "giveupgoal"]
1.935 + | "oops" => [xmle "postponegoal"]
1.936 + | "by" => [xmlc "proofstep" ("apply " ^ str),
1.937 + xmle "closegoal"] (* FIXME: tactic proofs only just now *)
1.938 + (* theories *)
1.939 + | "theory" => [make_theory str]
1.940 + (* goals *)
1.941 + | "lemma" => [make_opengoal str]
1.942 + | "theorem" => [make_opengoal str]
1.943 + | "corollary" => [make_opengoal str]
1.944 + (* literate text *)
1.945 + | "text" => [xmlc "litcomment" str]
1.946 + | "sect" => [xmlc "litcomment" ("ion " ^ str)]
1.947 + | "subsect" => [xmlc "litcomment" ("ion " ^ str)]
1.948 + | "subsubsect" => [xmlc "litcomment" ("ion " ^ str)]
1.949 + | "txt" => [xmlc "litcomment" str]
1.950 + | _ => [xmlc "proofstep" str] (* default for anything else *)
1.951 + end
1.952 +
1.953 +(* FIXME: need to handle parse errors gracefully below, perhaps returning partial parse *)
1.954 +(* NB: comments are ignored by below; not good if we use this to reconstruct script *)
1.955 +
1.956 +fun xmls_of_str str =
1.957 + let fun parse_loop (nm_lex_trs,xmls) =
1.958 + (case nm_lex_trs of
1.959 + [] => xmls
1.960 + | (nm,toks,tr)::rest =>
1.961 + let
1.962 + val xmls_tr = xmls_of_transition (nm,toks,tr)
1.963 + in
1.964 + parse_loop (rest, xmls @ xmls_tr)
1.965 + end)
1.966 + in
1.967 + parse_loop (OuterSyntax.read str, [])
1.968 + end
1.969 +
1.970 +
1.971 +fun parsescript str =
1.972 + issue_pgips [XML.element "parseresult" [] (xmls_of_str str)]
1.973 +
1.974 +end
1.975 +
1.976 +
1.977 +
1.978 +(**** PGIP: Isabelle -> Interface ****)
1.979 +
1.980 +val isabelle_pgml_version_supported = "1.0";
1.981 +val isabelle_pgip_version_supported = "1.0"
1.982 +
1.983 +fun usespgip () =
1.984 + issue_pgipe "usespgip" [("version", isabelle_pgip_version_supported)];
1.985 +
1.986 +fun usespgml () =
1.987 + issue_pgipe "usespgml" [("version", isabelle_pgml_version_supported)];
1.988 +
1.989 +fun hasprefs () =
1.990 + seq (fn (prefcat, prefs) =>
1.991 + issue_pgips [XML.element "hasprefs" [("prefcategory",prefcat)]
1.992 + (map (fn (name, (descr, (ty, (default,_),_))) =>
1.993 + XML.element "haspref" [("name", name),
1.994 + ("descr", descr),
1.995 + ("default", default)]
1.996 + [ty]) prefs)]) (!preferences);
1.997 +
1.998 +fun allprefs () = foldl (op @) ([], map snd (!preferences))
1.999 +
1.1000 +fun setpref name value =
1.1001 + (case assoc (allprefs(), name) of
1.1002 + None => warning ("Unknown pref: " ^ quote name)
1.1003 + | Some (_, (_, _, set)) => set value);
1.1004 +
1.1005 +fun getpref name =
1.1006 + (case assoc (allprefs(), name) of
1.1007 + None => warning ("Unknown pref: " ^ quote name)
1.1008 + | Some (_, (_, (_,get), _)) =>
1.1009 + issue_pgip "prefval" [("name", name)] (get ()));
1.1010 +
1.1011 +
1.1012 +
1.1013 +
1.1014 +
1.1015 +(**** PGIP: Interface -> Isabelle/Isar ****)
1.1016 +
1.1017 +exception PGIP of string;
1.1018 +exception PGIP_QUIT;
1.1019 +
1.1020 +(* Sending commands to Isar *)
1.1021 +
1.1022 +(* FIXME Makarius:
1.1023 + 'isarcmd': consider using 'Toplevel.>>>' instead of
1.1024 + 'Toplevel.loop'; unsure about the exact error behaviour required here;
1.1025 +*)
1.1026 +val isarcmd = Toplevel.loop o
1.1027 + (OuterSyntax.isar_readstring
1.1028 + (Position.name "PGIP message")) (* FIXME: could do better *)
1.1029 +
1.1030 +fun isarscript s = isarcmd s (* send a script command *)
1.1031 + (* was: (isarcmd s; issue_pgip "scriptinsert" [] (XML.text s)) *)
1.1032 +
1.1033 +
1.1034 +(* load an arbitrary (.thy or .ML) file *)
1.1035 +
1.1036 +fun use_thy_or_ml_file file =
1.1037 + let
1.1038 + val (path,extn) = Path.split_ext (Path.unpack file)
1.1039 + in
1.1040 + case extn of
1.1041 + "" => isarcmd ("use_thy " ^ (quote (Path.pack path)))
1.1042 + | "thy" => isarcmd ("use_thy " ^ (quote (Path.pack path)))
1.1043 + | "ML" => isarcmd ("use " ^ quote file)
1.1044 + (* instead of error we could guess theory? *)
1.1045 + | other => error ("Don't know how to read a file with extension " ^ other)
1.1046 + end
1.1047 +
1.1048 +
1.1049 +local
1.1050 + (* Proof control commands *)
1.1051 +
1.1052 + fun xmlattro attrs attr = assoc(attrs,attr)
1.1053 +
1.1054 + fun xmlattr attrs attr =
1.1055 + (case xmlattro attrs attr of
1.1056 + Some value => value
1.1057 + | None => raise PGIP ("Missing attribute: " ^ attr))
1.1058 +
1.1059 + fun xmltext [XML.Text text] = text
1.1060 + | xmltext ((XML.Text text)::ts) = text ^ " " ^ (xmltext ts) (* FIXME: space shouldn't be needed *)
1.1061 + | xmltext _ = raise PGIP "Expected text (PCDATA/CDATA)"
1.1062 +
1.1063 + val thyname_attr = "thyname"
1.1064 + val objtype_attr = "objtype"
1.1065 + val name_attr = "name"
1.1066 + val dirname_attr = "dir"
1.1067 + fun comment x = "(* " ^ x ^ " *)"
1.1068 +
1.1069 +(* return script portion corresponding to a PGIP command.
1.1070 + We only unparse proper proof commands.
1.1071 + (we might unparse gui opns too, if they didn't have opcmd settings?)
1.1072 +*)
1.1073 + fun unparse (elem,attrs,xmls) =
1.1074 + (case elem of
1.1075 + "opengoal" => "lemma " ^ (xmlattr attrs "thmname") ^ ": " ^
1.1076 + (quote (xmltext xmls))
1.1077 + (* FIXME: should maybe remove ^^^^^^^^^^
1.1078 + to provide for Isar's parenthetical phrases (is ...) *)
1.1079 + | "proofstep" => xmltext xmls
1.1080 + | "closegoal" => "done" (* FIXME: or qed? Maybe nothing? *)
1.1081 +
1.1082 + | "opentheory" => ("theory " ^ (xmlattr attrs thyname_attr) ^
1.1083 + " = " ^ (xmltext xmls) ^ ":")
1.1084 + | "closetheory" => "end"
1.1085 + | "postponegoal" => "sorry"
1.1086 + | "giveupgoal" => "oops"
1.1087 +
1.1088 + | "bindid" => (bindid (xmlattr attrs objtype_attr,
1.1089 + xmlattr attrs name_attr,
1.1090 + xmls))
1.1091 + | "comment" => comment (xmltext xmls)
1.1092 + | "litcomment" => xmltext xmls
1.1093 + | _ => error ("unparse called with improper proof command: " ^ elem))
1.1094 +
1.1095 + fun unparsecmds xmls =
1.1096 + let
1.1097 + fun upc (XML.Elem elt) = (unparse elt)
1.1098 + | upc (XML.Text t) = (warning ("unprasecmds: ignoring spurious text: " ^ t); "")
1.1099 + in
1.1100 + issue_pgip "unparseresult" []
1.1101 + (XML.text (cat_lines (map upc xmls))) (* FIXME: use cdata? *)
1.1102 + end
1.1103 +
1.1104 + (* parse URLs like "file://host/name.thy" *)
1.1105 + (* FIXME: instead of this, extend code in General/url.ML & use that. *)
1.1106 + fun decode_url url =
1.1107 + (let
1.1108 + val sep = find_index_eq ":" (explode url)
1.1109 + val proto = String.substring(url,0,sep)
1.1110 + val hostsep = find_index_eq "/" (drop (sep+3,explode url))
1.1111 + val host = String.substring(url,sep+3,hostsep-sep+4)
1.1112 + val doc = if (size url >= sep+hostsep+3) then
1.1113 + String.substring(url,sep+hostsep+4,size url-hostsep-sep-4)
1.1114 + else ""
1.1115 + in
1.1116 + (proto,host,doc)
1.1117 + end) handle Subscript => error ("Badly formed URL " ^ url)
1.1118 +
1.1119 + fun localfile_of_url url =
1.1120 + let
1.1121 + val (proto,host,name) = decode_url url
1.1122 + in
1.1123 + if (proto = "file" andalso
1.1124 + (host = "" orelse
1.1125 + host = "localhost" orelse
1.1126 + host = (getenv "HOSTNAME")))
1.1127 + then name
1.1128 + else error ("Cannot access non-local URL " ^ url)
1.1129 + end
1.1130 +
1.1131 + fun fileurl_of attrs = localfile_of_url (xmlattr attrs "url")
1.1132 +
1.1133 + val topthy = Toplevel.theory_of o Toplevel.get_state
1.1134 + val topthy_name = PureThy.get_name o topthy
1.1135 +
1.1136 + val currently_open_file = ref (None : string option)
1.1137 +in
1.1138 +
1.1139 +fun process_pgip_element pgipxml =
1.1140 + (case pgipxml of
1.1141 + (XML.Text t) => warning ("Ignored text in PGIP packet: \n" ^ t)
1.1142 + | (XML.Elem (xml as (elem, attrs, xmls))) => (case elem of
1.1143 +(* protocol config *)
1.1144 + "askpgip" => (usespgip (); send_pgip_config ())
1.1145 +| "askpgml" => usespgml ()
1.1146 +(* proverconfig *)
1.1147 +| "askprefs" => hasprefs ()
1.1148 +| "getpref" => getpref (xmlattr attrs name_attr)
1.1149 +| "setpref" => setpref (xmlattr attrs name_attr) (xmltext xmls)
1.1150 +(* provercontrol *)
1.1151 +| "proverinit" => isar_restart ()
1.1152 +| "proverexit" => isarcmd "quit"
1.1153 +| "startquiet" => isarcmd "disable_pr"
1.1154 +| "stopquiet" => isarcmd "enable_pr"
1.1155 +| "pgmlsymbolson" => (print_mode := (["xsymbols", "symbols"] @ ! print_mode))
1.1156 +| "pgmlsymbolsoff" => (print_mode := (Library.gen_rems
1.1157 + (op =) (! print_mode, ["xsymbols", "symbols"])))
1.1158 +(* provercmd: proper commands which belong in script *)
1.1159 +| "proofstep" => isarscript (unparse xml)
1.1160 +| "opengoal" => isarscript (unparse xml)
1.1161 +| "closegoal" => isarscript (unparse xml)
1.1162 +| "postponegoal" => isarscript (unparse xml)
1.1163 +| "giveupgoal" => isarscript (unparse xml)
1.1164 +| "comment" => isarscript (unparse xml)
1.1165 +| "litcomment" => isarscript (unparse xml)
1.1166 +(* provercmd: improper commands which *do not* belong in script *)
1.1167 +| "undostep" => isarcmd "ProofGeneral.undo"
1.1168 +| "abortgoal" => isarcmd "ProofGeneral.kill_proof"
1.1169 +| "forget" => error ("Not implemented")
1.1170 +| "restoregoal" => error ("Not implemented") (* could just treat as forget? *)
1.1171 +(* proofctxt: improper commands *)
1.1172 +| "askids" => askids (xmlattro attrs thyname_attr,
1.1173 + xmlattro attrs objtype_attr)
1.1174 +| "showid" => showid (xmlattro attrs thyname_attr,
1.1175 + xmlattr attrs objtype_attr,
1.1176 + xmlattr attrs name_attr)
1.1177 +| "parsescript" => parsescript (xmltext xmls)
1.1178 +| "unparsecmds" => unparsecmds xmls
1.1179 +| "showproofstate" => isarcmd "pr"
1.1180 +| "showctxt" => isarcmd "print_theory" (* more useful than print_context *)
1.1181 +| "searchtheorems" => isarcmd ("thms_containing " ^ (xmltext xmls))
1.1182 +| "setlinewidth" => isarcmd ("pretty_setmargin " ^ (xmltext xmls))
1.1183 +(* proofctxt: proper commands *)
1.1184 +| "bindid" => isarscript (unparse xml)
1.1185 +(* filecmd: proper commands *)
1.1186 +| "opentheory" => isarscript (unparse xml)
1.1187 +| "closetheory" => (isarscript (unparse xml);
1.1188 + writeln ("Theory "^(topthy_name())^" completed."))
1.1189 +(* filecmd: improper commands *)
1.1190 +| "aborttheory" => isarcmd ("init_toplevel")
1.1191 +| "retracttheory" => isarcmd ("kill_thy " ^
1.1192 + (quote (xmlattr attrs thyname_attr)))
1.1193 +| "loadfile" => use_thy_or_ml_file (fileurl_of attrs)
1.1194 +| "openfile" => (inform_file_retracted (fileurl_of attrs);
1.1195 + currently_open_file := Some (fileurl_of attrs))
1.1196 +| "closefile" => (case !currently_open_file of
1.1197 + Some f => (inform_file_processed f;
1.1198 + currently_open_file := None)
1.1199 + | None => raise PGIP ("closefile when no file is open!"))
1.1200 +| "abortfile" => (currently_open_file := None) (* might give error for no file open *)
1.1201 +| "changecwd" => ThyLoad.add_path (xmlattr attrs dirname_attr)
1.1202 +(* unofficial command for debugging *)
1.1203 +| "quitpgip" => raise PGIP_QUIT
1.1204 +| _ => raise PGIP ("Unrecognized PGIP element: " ^ elem)))
1.1205 +
1.1206 +fun process_pgip_tree s =
1.1207 + (pgip_refseq := None;
1.1208 + pgip_refid := None;
1.1209 + (case s of
1.1210 + XML.Elem ("pgip", attrs, pgips) =>
1.1211 + (let
1.1212 + val class = xmlattr attrs "class"
1.1213 + val _ = (pgip_refseq := xmlattro attrs "seq";
1.1214 + pgip_refid := xmlattro attrs "id")
1.1215 + in
1.1216 + if (class = "pa") then
1.1217 + seq process_pgip_element pgips
1.1218 + else
1.1219 + raise PGIP "PGIP packet for me should have class=\"pa\""
1.1220 + end)
1.1221 + | _ => raise PGIP "Invalid PGIP packet received")
1.1222 + handle (PGIP msg) =>
1.1223 + (error (msg ^ "\nPGIP error occured in XML text below:\n" ^
1.1224 + (XML.string_of_tree s))))
1.1225 +
1.1226 +(* for export to Emacs *)
1.1227 +(* val process_pgip = process_pgip_tree o XML.tree_of_string; *)
1.1228 +(* FIXME: for temporary compatibility with PG 3.4, we engage special characters
1.1229 + during output *)
1.1230 +fun process_pgip s =
1.1231 + (pgip_emacs_compatibility_flag := true;
1.1232 + process_pgip_tree (XML.tree_of_string s);
1.1233 + pgip_emacs_compatibility_flag := false)
1.1234 +end
1.1235 +
1.1236 +
1.1237 +
1.1238 +
1.1239 +(* PGIP loop: process PGIP input only *)
1.1240 +
1.1241 +local
1.1242 +(* NB: simple tty for now; later might read from other sources, open sockets, etc. *)
1.1243 +(* FIXME da: doesn't setting the stopper at a single element mean we have to
1.1244 + parse the whole tree on one go anyway? *)
1.1245 +val tty_src = Source.set_prompt ""
1.1246 + (Source.source Symbol.stopper (XML.parse_elem >> single)
1.1247 + None Source.tty);
1.1248 +
1.1249 +(* FIXME: Makarius:
1.1250 + 'read_pgip()': some content may be left in the internal buffer after
1.1251 + Source.get_single, which will got lost between calls; try to avoid
1.1252 + building the tty source over and over again;
1.1253 +*)
1.1254 +
1.1255 +fun read_pgip () = Source.get_single tty_src
1.1256 +
1.1257 +fun loop () =
1.1258 + let
1.1259 + val _ = issue_pgipe "ready" []
1.1260 + in
1.1261 + case (read_pgip()) of
1.1262 + None => ()
1.1263 + | Some (pgip,_) => (process_pgip_tree pgip; loop()) handle e => handler e
1.1264 + end handle e => handler e
1.1265 +
1.1266 +and handler e =
1.1267 + case e of
1.1268 + PGIP_QUIT => ()
1.1269 + | ERROR => loop() (* message already given *)
1.1270 + | Interrupt => (error "Interrupt during PGIP processing"; loop())
1.1271 + | Toplevel.UNDEF => (error "No working context defined"; loop()) (* usually *)
1.1272 + | e => (error (Toplevel.exn_message e); loop())
1.1273 + (* Also seen: Scan.FAIL (not exported from Scan -- needs catching in xml.ML) *)
1.1274 +in
1.1275 + val pgip_toplevel = loop
1.1276 +end
1.1277 +
1.1278 +
1.1279 +(* additional outer syntax for Isar *)
1.1280
1.1281 local structure P = OuterParse and K = OuterSyntax.Keyword in
1.1282
1.1283 -val undoP =
1.1284 +val undoP = (* undo without output *)
1.1285 OuterSyntax.improper_command "ProofGeneral.undo" "(internal)" K.control
1.1286 (Scan.succeed (Toplevel.no_timing o IsarCmd.undo));
1.1287
1.1288 @@ -455,10 +1126,16 @@
1.1289
1.1290 val initialized = ref false;
1.1291
1.1292 -fun init isar =
1.1293 +fun set_prompts true _ = ml_prompts "ML> " "ML# "
1.1294 + | set_prompts false true = ml_prompts "PGIP-ML>" "PGIP-ML# "
1.1295 + | set_prompts false false =
1.1296 + ml_prompts ("> " ^ oct_char "372") ("- " ^ oct_char "373");
1.1297 +
1.1298 +fun init_setup isar pgip =
1.1299 (conditional (not (! initialized)) (fn () =>
1.1300 (if isar then setmp warning_fn (K ()) init_outer_syntax () else ();
1.1301 setup_xsymbols_output ();
1.1302 + setup_pgml_output ();
1.1303 setup_messages ();
1.1304 setup_state ();
1.1305 setup_thy_loader ();
1.1306 @@ -466,27 +1143,43 @@
1.1307 set initialized; ()));
1.1308 sync_thy_loader ();
1.1309 print_mode := proof_generalN :: (! print_mode \ proof_generalN);
1.1310 + if pgip then
1.1311 + print_mode := pgmlN :: (pgmlatomsN :: (! print_mode \ pgmlN \ pgmlatomsN))
1.1312 + else ();
1.1313 set quick_and_dirty;
1.1314 ThmDeps.enable ();
1.1315 - if isar then ml_prompts "ML> " "ML# "
1.1316 - else ml_prompts ("> " ^ oct_char "372") ("- " ^ oct_char "373");
1.1317 - if isar then (welcome (); Isar.sync_main ()) else isa_restart ());
1.1318 + set_prompts isar pgip;
1.1319 + pgip_active := pgip)
1.1320
1.1321 +fun init isar =
1.1322 + (init_setup isar false;
1.1323 + if isar then ((* da: this welcome is problematic: clashes with welcome
1.1324 + issued for PG anyway.
1.1325 + welcome (); *)
1.1326 + Isar.sync_main ()) else isa_restart ());
1.1327
1.1328 +fun init_pgip false = panic "Sorry, PGIP not supported for Isabelle/classic mode."
1.1329 + | init_pgip true = (init_setup true true; pgip_toplevel());
1.1330
1.1331 -(** generate keyword classification file **)
1.1332 +
1.1333 +
1.1334 +(** generate keyword classification elisp file **)
1.1335
1.1336 local
1.1337
1.1338 val regexp_meta = explode ".*+?[]^$";
1.1339 -val regexp_quote = implode o map (fn c => if c mem regexp_meta then "\\\\" ^ c else c) o explode;
1.1340 +val regexp_quote =
1.1341 + implode o map (fn c => if c mem regexp_meta then "\\\\" ^ c else c)
1.1342 + o explode;
1.1343
1.1344 fun defconst name strs =
1.1345 "\n(defconst isar-keywords-" ^ name ^
1.1346 "\n '(" ^ space_implode "\n " (map (quote o regexp_quote) strs) ^ "))\n";
1.1347
1.1348 fun make_elisp_commands commands kind =
1.1349 - defconst kind (mapfilter (fn (c, _, k, _) => if k = kind then Some c else None) commands);
1.1350 + defconst kind (mapfilter
1.1351 + (fn (c, _, k, _) => if k = kind then Some c else None)
1.1352 + commands);
1.1353
1.1354 fun make_elisp_syntax (keywords, commands) =
1.1355 ";;\n\
1.1356 @@ -496,7 +1189,7 @@
1.1357 \;; $" ^ "Id$\n\
1.1358 \;;\n" ^
1.1359 defconst "major" (map #1 commands) ^
1.1360 - defconst "minor" (filter Syntax.is_ascii_identifier keywords) ^
1.1361 + defconst "minor" (filter Syntax.is_identifier keywords) ^
1.1362 implode (map (make_elisp_commands commands) OuterSyntax.Keyword.kinds) ^
1.1363 "\n(provide 'isar-keywords)\n";
1.1364
1.1365 @@ -505,8 +1198,9 @@
1.1366 fun write_keywords s =
1.1367 (init_outer_syntax ();
1.1368 File.write (Path.unpack ("isar-keywords" ^ (if s = "" then "" else "-" ^ s) ^".el"))
1.1369 - (make_elisp_syntax (OuterSyntax.dest_keywords (), OuterSyntax.dest_parsers ())));
1.1370 + (make_elisp_syntax (OuterSyntax.dest_keywords (),
1.1371 + OuterSyntax.dest_parsers ())));
1.1372
1.1373 end;
1.1374
1.1375 -end;
1.1376 +end