Added show_var_qmarks flag.
(* Title: Pure/proof_general.ML
ID: $Id$
Author: David Aspinall and Markus Wenzel
Isabelle configuration for Proof General (see http://proofgeneral.inf.ed.ac.uk)
Includes support for PGIP control language for Isabelle/Isar.
===========================================================================
NOTE: With this version you will lose support for the Isabelle
settings menu in the currently released version of Proof General (3.5).
No other changes should be visible in the Emacs interface.
The 3.6pre pre-release versions of Emacs Proof General now support the
new PGIP format for preferences and restore the settings menu.
Please visit http://proofgeneral.inf.ed.ac.uk/develdownload
===========================================================================
STATUS: this version is an experimental version that supports PGIP 2.X.
*)
signature PROOF_GENERAL =
sig
val setup: (theory -> theory) list
val update_thy_only: string -> unit
val try_update_thy_only: string -> unit
val inform_file_retracted: string -> unit
val inform_file_processed: string -> unit
val preferences:
(string *
(string *
(string *
(string * (string * (unit -> string)) *
(string -> unit)))) list) list ref
val process_pgip: string -> unit
val thms_containing: string list -> unit
val help: unit -> unit
val show_context: unit -> theory
val kill_goal: unit -> unit
val repeat_undo: int -> unit
val isa_restart: unit -> unit
val full_proofs: bool -> unit
val isarcmd: string -> unit
val init: bool -> unit
val init_pgip: bool -> unit
val write_keywords: string -> unit
val xmls_of_str : string -> string list (* temp for testing parser *)
end;
structure ProofGeneral : PROOF_GENERAL =
struct
structure P = OuterParse
(* PGIP messaging mode (independent of PGML output) *)
val pgip_active = ref false;
val pgip_emacs_compatibility_flag = ref false;
fun pgip () = (!pgip_active);
fun pgip_emacs_compatibility () = (!pgip_emacs_compatibility_flag);
(* print modes *)
val proof_generalN = "ProofGeneral"; (* token markup (colouring vars, etc.) *)
val xsymbolsN = Symbol.xsymbolsN; (* XSymbols symbols *)
val pgmlN = "PGML"; (* XML escapes and PGML symbol elements *)
val pgmlatomsN = "PGMLatoms"; (* variable kind decorations *)
val thm_depsN = "thm_deps"; (* meta-information about theorem deps *)
fun pgml () = pgmlN mem_string ! print_mode;
(* text output: print modes for xsymbol and PGML *)
local
fun xsym_output "\\" = "\\\\"
| xsym_output s = if Symbol.is_raw s then Symbol.decode_raw s else s;
fun xsymbols_output s =
if xsymbolsN mem_string ! print_mode andalso exists_string (equal "\\") s then
let val syms = Symbol.explode s
in (implode (map xsym_output syms), real (Symbol.length syms)) end
else Symbol.default_output s;
fun pgml_sym s =
(case Symbol.decode s of
(* NB: an alternative here would be to output the default print mode alternative
in the element content, but unfortunately print modes are not that fine grained. *)
Symbol.Char s => XML.text s
| Symbol.Sym sn => XML.element "sym" [("name", sn)] [XML.text s]
| Symbol.Ctrl sn => XML.element "ctrl" [("name", sn)] [XML.text s] (* FIXME: no such PGML! *)
| Symbol.Raw s => s);
fun pgml_output str =
let val syms = Symbol.explode str
in (implode (map pgml_sym syms), real (Symbol.length syms)) end;
in
fun setup_xsymbols_output () =
Output.add_mode
xsymbolsN
(xsymbols_output, Symbol.default_indent, Symbol.encode_raw);
fun setup_pgml_output () =
Output.add_mode
pgmlN
(pgml_output, Symbol.default_indent, Symbol.encode_raw);
end;
(* token translations *)
local
val end_tag = oct_char "350";
val class_tag = ("class", oct_char "351");
val tfree_tag = ("tfree", oct_char "352");
val tvar_tag = ("tvar", oct_char "353");
val free_tag = ("free", oct_char "354");
val bound_tag = ("bound", oct_char "355");
val var_tag = ("var", oct_char "356");
val skolem_tag = ("skolem", oct_char "357");
fun xml_atom kind x = XML.element "atom" [("kind", kind)] [XML.text x];
fun tagit (kind, bg_tag) x =
(if Output.has_mode pgmlatomsN then
xml_atom kind x
else bg_tag ^ x ^ end_tag,
real (Symbol.length (Symbol.explode x)));
fun free_or_skolem x =
(case try Syntax.dest_skolem x of
None => tagit free_tag x
| Some x' => tagit skolem_tag x');
fun var_or_skolem s =
(case Syntax.read_var s of
Var ((x, i), _) =>
(case try Syntax.dest_skolem x of
None => tagit var_tag s
| Some x' => tagit skolem_tag (Syntax.string_of_vname (x', i)))
| _ => tagit var_tag s);
val proof_general_trans =
Syntax.tokentrans_mode proof_generalN
[("class", tagit class_tag),
("tfree", tagit tfree_tag),
("tvar", tagit tvar_tag),
("free", free_or_skolem),
("bound", tagit bound_tag),
("var", var_or_skolem)];
in val setup = [Theory.add_tokentrfuns proof_general_trans] end;
(* assembling PGIP packets *)
val pgip_refseq = ref None : string option ref
val pgip_refid = ref None : string option ref
local
val myseq_no = ref 1; (* PGIP packet counter *)
val pgip_class = "pg"
val pgip_origin = "Isabelle/Isar"
val pgip_id = (getenv "HOSTNAME") ^ "/" ^ (getenv "USER") ^ "/" ^
(Time.toString(Time.now()))
(* FIXME: PPID is empty for me: any way to get process ID? *)
fun assemble_pgips pgips =
XML.element
"pgip"
([("class", pgip_class),
("origin", pgip_origin),
("id", pgip_id)] @
(if_none (apsome (single o (pair "refseq")) (!pgip_refseq)) []) @
(if_none (apsome (single o (pair "refid")) (!pgip_refid)) []) @
[("seq", string_of_int (Library.inc myseq_no))])
pgips
in
fun decorated_output bg en prfx =
writeln_default o enclose bg en o prefix_lines prfx;
(* FIXME: see Rev 1.48 [PG CVS] for cleaner version of this which can be used
for PG 4.0 which processes PGIP without needing special chars. *)
fun issue_pgips ps =
if pgip_emacs_compatibility() then
decorated_output (* add urgent message annotation *)
(oct_char "360") (oct_char "361") ""
(assemble_pgips ps)
else
writeln_default (assemble_pgips ps)
fun assemble_pgip resp attrs s = assemble_pgips [XML.element resp attrs [s]]
fun assemble_pgipe resp attrs = assemble_pgips [XML.element resp attrs []]
(* FIXME: need to add stuff to gather PGIPs here *)
fun issue_pgip resp attrs txt =
if pgip_emacs_compatibility() then
decorated_output (* add urgent message annotation *)
(oct_char "360") (oct_char "361") ""
(assemble_pgip resp attrs txt)
else
writeln_default (assemble_pgip resp attrs txt)
(* FIXME: temporarily to support PG 3.4. *)
fun issue_pgip_maybe_decorated bg en resp attrs s =
if pgip_emacs_compatibility() then
(* in PGIP mode, but using escape characters as well. *)
writeln_default (enclose bg en (assemble_pgip resp attrs s))
else
issue_pgip resp attrs s
fun issue_pgipe resp attrs = writeln_default (assemble_pgipe resp attrs)
end
(* messages and notification *)
local
val delay_msgs = ref false (* whether to accumulate messages *)
val delayed_msgs = ref []
in
fun message resp attrs bg en prfx s =
if pgip() then
(if (!delay_msgs) then
delayed_msgs := (resp,attrs,prefix_lines prfx s)::(!delayed_msgs) (* nb: no decs *)
else
issue_pgip_maybe_decorated bg en resp attrs
(XML.element "pgmltext" [] [prefix_lines prfx s]))
else
decorated_output bg en prfx s;
fun start_delay_msgs () = (delay_msgs := true;
delayed_msgs := [])
fun end_delayed_msgs () =
(delay_msgs := false;
map (fn (resp,attrs,s) => XML.element resp attrs [XML.element "pgmltext" [] [s]]) (!delayed_msgs))
end
local
val display_area = ("area", "display")
val message_area = ("area", "message")
val internal_category = ("messagecategory", "internal")
val info_category = ("messagecategory", "information")
val tracing_category = ("messagecategory", "tracing")
val urgent_indication = ("urgent", "y")
val nonfatal = ("fatality", "nonfatal")
val fatal = ("fatality", "fatal")
val panic = ("fatality", "panic")
val thyname_attr = pair "thyname"
val url_attr = pair "url"
fun localfile_url_attr path = url_attr ("file:///" ^ path)
in
fun setup_messages () =
(writeln_fn := message "normalresponse" [message_area] "" "" "";
priority_fn := message "normalresponse" [message_area, urgent_indication]
(oct_char "360") (oct_char "361") "";
tracing_fn := message "normalresponse" [message_area, tracing_category]
(oct_char "360" ^ oct_char "375") (oct_char "361") "";
info_fn := message "normalresponse" [message_area, info_category]
(oct_char "362") (oct_char "363") "+++ ";
debug_fn := message "normalresponse" [message_area, internal_category]
(oct_char "362") (oct_char "363") "+++ ";
warning_fn := message "errorresponse" [nonfatal]
(oct_char "362") (oct_char "363") "### ";
error_fn := message "errorresponse" [fatal]
(oct_char "364") (oct_char "365") "*** ";
panic_fn := message "errorresponse" [panic]
(oct_char "364") (oct_char "365") "!!! ")
(* accumulate printed output in a single PGIP response (inside <pgmltext>) *)
fun with_displaywrap (elt,attrs) dispfn =
let
val lines = ref ([] : string list);
fun wlgrablines s = (lines:= (s :: (!lines)))
in
(setmp writeln_fn wlgrablines dispfn ();
(* FIXME: XML.element here inefficient, should use stream output *)
issue_pgip elt attrs (XML.element "pgmltext" [] (!lines)))
end
val emacs_notify = decorated_output (oct_char "360") (oct_char "361") "";
fun tell_clear_goals () =
if pgip() then
issue_pgipe "cleardisplay" [display_area]
else
emacs_notify "Proof General, please clear the goals buffer.";
fun tell_clear_response () =
if pgip() then
issue_pgipe "cleardisplay" [message_area]
else
emacs_notify "Proof General, please clear the response buffer.";
fun tell_file_loaded path =
if pgip() then
issue_pgipe "informtheoryloaded" (* FIXME: get thy name from info here? *)
[thyname_attr (XML.text (File.sysify_path path)),
localfile_url_attr (XML.text (File.sysify_path path))]
else
emacs_notify ("Proof General, this file is loaded: "
^ quote (File.sysify_path path));
fun tell_file_retracted path =
if pgip() then
issue_pgipe "informtheoryretracted" (* FIXME: get thy name from info here? *)
[thyname_attr (XML.text (File.sysify_path path)),
localfile_url_attr (XML.text (File.sysify_path path))]
else
emacs_notify ("Proof General, you can unlock the file "
^ quote (File.sysify_path path));
(* theory / proof state output *)
local
fun tmp_markers f = setmp Display.current_goals_markers
(oct_char "366", oct_char "367", "") f ()
fun statedisplay prts =
issue_pgip "proofstate" []
(XML.element "pgml" []
[XML.element "statedisplay"
[]
[(Pretty.output (Pretty.chunks prts))]])
fun print_current_goals n m st =
if pgml () then statedisplay (Display.pretty_current_goals n m st)
else tmp_markers (fn () => Display.print_current_goals_default n m st)
fun print_state b st =
if pgml () then statedisplay (Toplevel.pretty_state b st)
else tmp_markers (fn () => Toplevel.print_state_default b st)
in
fun setup_state () =
(Display.print_current_goals_fn := print_current_goals;
Toplevel.print_state_fn := print_state;
(* FIXME: check next octal char won't appear in pgip? *)
Toplevel.prompt_state_fn := (suffix (oct_char "372") o
Toplevel.prompt_state_default));
end
end
(* misc commands for ProofGeneral/isa *)
fun thms_containing ss =
ProofContext.print_thms_containing (ProofContext.init (the_context ())) None ss;
val welcome = priority o Session.welcome;
val help = welcome;
val show_context = Context.the_context;
fun kill_goal () = (Goals.reset_goals (); tell_clear_goals ());
fun no_print_goals f = setmp Display.print_current_goals_fn (fn _ => fn _ => fn _ => ()) f;
fun repeat_undo 0 = ()
| repeat_undo 1 = undo ()
| repeat_undo n = (no_print_goals undo (); repeat_undo (n - 1));
(* theory loader actions *)
local
fun add_master_files name files =
let val masters = [ThyLoad.thy_path name, ThyLoad.ml_path name]
in masters @ gen_rems (op = o pairself Path.base) (files, masters) end;
fun trace_action action name =
if action = ThyInfo.Update then
seq tell_file_loaded (ThyInfo.loaded_files name)
else if action = ThyInfo.Outdate orelse action = ThyInfo.Remove then
seq tell_file_retracted (add_master_files name (ThyInfo.loaded_files name))
else ();
in
fun setup_thy_loader () = ThyInfo.add_hook trace_action;
fun sync_thy_loader () = seq (trace_action ThyInfo.Update) (ThyInfo.names ());
end;
(* prepare theory context *)
val thy_name = Path.pack o #1 o Path.split_ext o Path.base o Path.unpack;
val update_thy_only = setmp MetaSimplifier.trace_simp
false ThyInfo.update_thy_only;
fun which_context () =
(case Context.get_context () of
Some thy => " Using current (dynamic!) one: " ^
(case try PureThy.get_name thy of Some name => quote name | None => "<unnamed>")
| None => "");
fun try_update_thy_only file =
ThyLoad.cond_add_path (Path.dir (Path.unpack file)) (fn () =>
let val name = thy_name file in
if is_some (ThyLoad.check_file None (ThyLoad.thy_path name))
then update_thy_only name
else warning ("Unkown theory context of ML file." ^ which_context ())
end) ();
(* get informed about files *)
val inform_file_retracted =
ThyInfo.if_known_thy ThyInfo.remove_thy o thy_name;
val inform_file_processed =
ThyInfo.if_known_thy ThyInfo.touch_child_thys o thy_name;
fun proper_inform_file_processed file state =
let val name = thy_name file in
if Toplevel.is_toplevel state andalso ThyInfo.known_thy name then
(ThyInfo.touch_child_thys name;
transform_error ThyInfo.pretend_use_thy_only name handle ERROR_MESSAGE msg =>
(warning msg; warning ("Failed to register theory: " ^ quote name);
tell_file_retracted (Path.base (Path.unpack file))))
else raise Toplevel.UNDEF
end;
fun vacuous_inform_file_processed file state =
(warning ("No theory " ^ quote (thy_name file));
tell_file_retracted (Path.base (Path.unpack file)));
(* restart top-level loop (keeps most state information) *)
local
fun restart isar =
(if isar then tell_clear_goals () else kill_goal ();
tell_clear_response ();
welcome ());
in
fun isa_restart () = restart false;
fun isar_restart () = (sync_thy_loader (); restart true; raise Toplevel.RESTART);
end;
fun full_proofs true = proofs := 2
| full_proofs false = proofs := 1;
(* theorem dependency output *)
local
val spaces_quote = space_implode " " o map quote;
fun thm_deps_message (thms, deps) =
if pgip() then
issue_pgips
[XML.element
"metainforesponse" (* FIXME: get thy name from info here? *)
[("infotype", "isabelle_theorem_dependencies")]
[XML.element "value" [("name", "thms")] [XML.text thms],
XML.element "value" [("name", "deps")] [XML.text deps]]]
else emacs_notify
("Proof General, theorem dependencies of "
^ thms ^ " are " ^ deps)
fun tell_thm_deps ths =
conditional (thm_depsN mem_string ! print_mode) (fn () =>
let
val names = map Thm.name_of_thm ths \ "";
val deps = Symtab.keys (foldl (uncurry Proofterm.thms_of_proof)
(Symtab.empty, map Thm.proof_of ths)) \ "";
in
if null names orelse null deps then ()
else thm_deps_message (spaces_quote names, spaces_quote deps)
end);
in
fun setup_present_hook () =
Present.add_hook (fn _ => fn res => tell_thm_deps (flat (map #2 res)));
end;
(*** Preferences ***)
local
val pgipnat = XML.element "pgipint" [("min", "0")] []
fun pgipnatmax max = XML.element "pgipint" [("min", "0"),
("max", string_of_int max)] []
val pgipbool = XML.element "pgipbool" [] []
fun withdefault f = (f(), f)
in
fun nat_option r = (pgipnat,
withdefault (fn () => string_of_int (!r)),
(fn s => (case Syntax.read_nat s of
None => error ("nat_option: illegal value " ^ s)
| Some i => r := i)));
fun bool_option r = (pgipbool,
withdefault (fn () => Bool.toString (!r)),
(fn "false" => r := false | "true" => r := true
| x => error ("bool_option: illegal value" ^ x)));
val proof_option = (pgipbool,
withdefault (fn () => Bool.toString (!proofs >= 2)),
(fn "false" => proofs := 1 | "true" => proofs := 2
| x => error ("proof_option: illegal value" ^ x)));
val thm_deps_option = (pgipbool,
withdefault (fn () => Bool.toString (Output.has_mode "thm_deps")),
(fn "false" => print_mode := ((!print_mode) \ "thm_deps")
| "true" => print_mode := ("thm_deps" ins (!print_mode))
| x => error ("thm_deps_option: illegal value " ^ x)));
local
val pg_print_depth_val = ref 10
fun pg_print_depth n = (print_depth n; pg_print_depth_val := n)
in
val print_depth_option = (pgipnat,
withdefault (fn () => string_of_int (!pg_print_depth_val)),
(fn s => (case Syntax.read_nat s of
None => error ("print_depth_option: illegal value" ^ s)
| Some i => pg_print_depth i)))
end
val preferences = ref
[("Display",
[("show-types",
("Include types in display of Isabelle terms",
bool_option show_types)),
("show-sorts",
("Include sorts in display of Isabelle terms",
bool_option show_sorts)),
("show-consts",
("Show types of consts in Isabelle goal display",
bool_option show_consts)),
("long-names",
("Show fully qualified names in Isabelle terms", bool_option long_names)),
("show-brackets",
("Show full bracketing in Isabelle terms",
bool_option show_brackets)),
("show-main-goal",
("Show main goal in proof state display", bool_option Proof.show_main_goal)),
("eta-contract",
("Print terms eta-contracted",
bool_option Syntax.eta_contract))]),
("Advanced Display",
[("goals-limit",
("Setting for maximum number of goals printed",
nat_option goals_limit)),
("prems-limit",
("Setting for maximum number of premises printed",
nat_option ProofContext.prems_limit)),
("print-depth",
("Setting for the ML print depth",
print_depth_option)),
("show-var-qmarks",
("Show leading question mark of variable name",
bool_option show_var_qmarks))]),
("Tracing",
[("trace-simplifier",
("Trace simplification rules.",
bool_option trace_simp)),
("trace-rules", ("Trace application of the standard rules",
bool_option trace_rules)),
("trace-unification",
("Output error diagnostics during unification",
bool_option Pattern.trace_unify_fail)),
("global-timing",
("Whether to enable timing in Isabelle.",
bool_option Output.timing))]),
("Proof",
[("quick-and-dirty",
("Take a few (interactive-only) short cuts",
bool_option quick_and_dirty)),
("full-proofs",
("Record full proof objects internally",
proof_option)),
("theorem-dependencies",
("Track theorem dependencies within Proof General",
thm_deps_option)),
("skip-proofs",
("Skip all proof scripts (interactive-only)",
bool_option Toplevel.skip_proofs))])
];
end
(* Configuration: GUI config, proverinfo messages *)
local
val config_file = "~~/lib/ProofGeneral/pgip_isar.xml"
val name_attr = pair "name"
val version_attr = pair "version"
val isabelle_www = "http://isabelle.in.tum.de/"
in
fun send_pgip_config () =
let
val path = Path.unpack config_file
val exists = File.exists path
val proverinfo =
XML.element "proverinfo"
[("name",Session.name()), ("version", version),
("url", isabelle_www), ("filenameextns", ".thy;")]
[XML.element "welcomemsg" [] [XML.text (Session.welcome())],
XML.element "helpdoc"
(* NB: would be nice to generate/display docs from isatool
doc, but that program may not be running on same machine;
front end should be responsible for launching viewer, etc. *)
[("name", "Isabelle/HOL Tutorial"),
("descr", "A Gentle Introduction to Isabelle/HOL"),
("url", "http://isabelle.in.tum.de/dist/Isabelle2004/doc/tutorial.pdf")]
[]]
in
if exists then
(issue_pgips [proverinfo]; issue_pgips [File.read path])
else panic ("PGIP configuration file " ^ config_file ^ " not found")
end;
end
(* PGIP identifier tables (prover objects). [incomplete] *)
local
val objtype_thy = "theory"
val objtype_thm = "theorem"
val objtype_term = "term"
val objtype_type = "type"
fun xml_idtable ty ctx ids =
let
fun ctx_attr (Some c)= [("context", c)]
| ctx_attr None = []
fun xmlid x = XML.element "identifier" [] [XML.text x];
in
XML.element "idtable" (("objtype", ty)::ctx_attr ctx)
(map xmlid ids)
end
in
fun setids t = issue_pgip "setids" [] t
fun addids t = issue_pgip "addids" [] t
fun delids t = issue_pgip "delids" [] t
fun delallids ty = setids (xml_idtable ty None [])
fun send_thy_idtable ctx thys = setids (xml_idtable objtype_thy ctx thys)
fun clear_thy_idtable () = delallids objtype_thy
fun send_thm_idtable ctx thy =
addids (xml_idtable objtype_thm ctx (map fst (PureThy.thms_of thy)));
fun clear_thm_idtable () = delallids objtype_thm
(* fun send_type_idtable thy = TODO, it's a bit low-level messy
& maybe not so useful anyway *)
end
(* Response to interface queries about known objects *)
local
val topthy = Toplevel.theory_of o Toplevel.get_state
fun pthm thy name = print_thm (get_thm thy (name, None))
fun idvalue tp nm = ("idvalue",[("objtype",tp),("name",nm)])
in
fun askids (None, Some "theory") = send_thy_idtable None (ThyInfo.names())
| askids (None, None) = send_thy_idtable None (ThyInfo.names())
(* only theories known in top context *)
| askids (Some thy, Some "theory") = send_thy_idtable (Some thy) (ThyInfo.get_preds thy)
| askids (Some thy, Some "theorem") = send_thm_idtable (Some thy) (ThyInfo.get_theory thy)
| askids (Some thy, None) = (send_thy_idtable (Some thy) (ThyInfo.get_preds thy);
send_thm_idtable (Some thy) (ThyInfo.get_theory thy))
| askids (_, Some ot) = error ("No objects of type "^(quote ot)^" are available here.")
fun showid (_, "theory", n) =
with_displaywrap (idvalue "theory" n) (fn ()=>(print_theory (ThyInfo.get_theory n)))
| showid (Some thy, "theorem", t) =
with_displaywrap (idvalue "theorem" t) (fn ()=>(pthm (ThyInfo.get_theory thy) t))
| showid (None, "theorem", t) =
with_displaywrap (idvalue "theorem" t) (fn ()=>pthm (topthy()) t)
| showid (_, ot, _) = error ("Cannot show objects of type "^ot)
end
(** Parsing proof scripts without execution **)
(* Notes.
This is quite tricky, because 1) we need to put back whitespace which
was removed during parsing so we can provide markup around commands;
2) parsing is intertwined with execution in Isar so we have to repeat
the parsing to extract interesting parts of commands. The trace of
tokens parsed which is now recorded in each transition (added by
Markus June '04) helps do this, but the mechanism is still a bad mess.
If we had proper parse trees it would be easy, although having a
fixed type of trees might be tricky with Isar's extensible parser.
Probably the best solution is to produce the meta-information at
the same time as the parse, for each command, e.g. by recording a
list of (name,objtype) pairs which record the bindings created by
a command. This would require changing the interfaces in
outer_syntax.ML (or providing new ones),
datatype metainfo = Binding of string * string (* name, objtype *)
val command_withmetainfo: string -> string -> string ->
(token list ->
((Toplevel.transition -> Toplevel.transition) * metainfo list) *
token list) -> parser
We'd also like to render terms as they appear in output, but this
will be difficult because inner syntax is extensible and we don't
have the correct syntax to hand when just doing outer parsing
without execution. A reasonable approximation could
perhaps be obtained by using the syntax of the current context.
However, this would mean more mess trying to pick out terms,
so at this stage a more serious change to the Isar functions
seems necessary.
*)
local
fun markup_text str elt = [XML.element elt [] [XML.text str]]
fun markup_text_attrs str elt attrs = [XML.element elt attrs [XML.text str]]
fun empty elt = [XML.element elt [] []]
fun whitespace str = XML.element "whitespace" [] [XML.text str]
(* an extra token is needed to terminate the command *)
val sync = OuterSyntax.scan "\\<^sync>";
fun named_item_elt_with nameattr toks str elt nameP objtyp =
let
val name = (fst (nameP (toks@sync)))
handle _ => (error ("Error occurred in name parser for " ^ elt ^
"(objtype: " ^ objtyp ^ ")");
"")
in
[XML.element elt
((if name="" then [] else [(nameattr, name)])@
(if objtyp="" then [] else [("objtype", objtyp)]))
([XML.text str])]
end
val named_item_elt = named_item_elt_with "name"
val thmnamed_item_elt = named_item_elt_with "thmname"
fun parse_warning msg = warning ("script->PGIP markup parser: " ^ msg)
(* FIXME: allow dynamic extensions to language here: we need a hook in
outer_syntax.ML to reset this table. *)
val keywords_classification_table = ref (None:(string Symtab.table) option)
fun get_keywords_classification_table () =
case (!keywords_classification_table) of
Some t => t
| None => (let
val tab = foldl (fn (tab,(c,_,k,_))=>Symtab.update((c,k),tab))
(Symtab.empty,OuterSyntax.dest_parsers())
in (keywords_classification_table := Some tab; tab) end)
fun xmls_of_thy_begin (name,toks,str) = (* see isar_syn.ML/theoryP *)
let
val ((thyname,imports,files),_) = ThyHeader.args (toks@sync)
in
markup_text_attrs str "opentheory"
([("thyname",thyname)] @
(if imports=[] then [] else
[("parentnames", (space_implode ";" imports) ^ ";")]))
end
fun xmls_of_thy_decl (name,toks,str) = (* see isar_syn.ML/thy_decl cases *)
let
(* NB: PGIP only deals with single name bindings at the moment;
potentially we could markup grouped definitions several times but
that might suggest the wrong structure to the editor?
Better alternative would be to put naming closer around text,
but to do that we'd be much better off modifying the real parser
instead of reconstructing it here. *)
val plain_items = (* no names, unimportant names, or too difficult *)
["defaultsort","arities","judgement","finalconsts",
"syntax", "nonterminals", "translations",
"global", "local", "hide",
"ML_setup", "setup", "method_setup",
"parse_ast_translation", "parse_translation", "print_translation",
"typed_print_translation", "print_ast_translation", "token_translation",
"oracle",
"declare"]
val plain_item = markup_text str "theoryitem"
val comment_item = markup_text str "litcomment"
val named_item = named_item_elt toks str "theoryitem"
val opt_overloaded = P.opt_keyword "overloaded";
val thmnameP = (* see isar_syn.ML/theoremsP *)
let
val name_facts = P.and_list1 ((P.opt_thm_name "=" --| P.xthms1) >> #1)
val theoremsP = P.locale_target |-- name_facts >> (fn [] => "" | x::_ => x)
in
theoremsP
end
in
(* TODO: ideally we would like to render terms properly, just as they are
in output. This implies using PGML for symbols and variables/atoms.
BUT it's rather tricky without having the correct concrete syntax to hand,
and even if we did, we'd have to mess around here a whole lot more first
to pick out the terms from the syntax. *)
if (name mem plain_items) then plain_item
else case name of
"text" => comment_item
| "text_raw" => comment_item
| "typedecl" => named_item (P.type_args |-- P.name) "type"
| "types" => named_item (P.type_args |-- P.name) "type"
| "classes" => named_item P.name "class"
| "classrel" => named_item P.name "class"
| "consts" => named_item (P.const >> #1) "term"
| "axioms" => named_item (P.spec_name >> (#1 o #1)) "theorem"
| "defs" => named_item (opt_overloaded |-- P.spec_name >> (#1 o #1)) "theorem"
| "constdefs" => named_item P.name (* FIXME: heavily simplified/wrong *) "term"
| "theorems" => named_item thmnameP "thmset"
| "lemmas" => named_item thmnameP "thmset"
| "oracle" => named_item P.name "oracle"
| "locale" => named_item ((P.opt_keyword "open" >> not) |-- P.name) "locale"
| _ => (parse_warning ("Unrecognized thy-decl command: " ^ name); plain_item)
end
fun xmls_of_thy_goal (name,toks,str) =
let
(* see isar_syn.ML/gen_theorem *)
val statement = P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.propp);
val general_statement =
statement >> pair [] || Scan.repeat P.locale_elem_or_expr -- (P.$$$ "shows" |-- statement);
val gen_theoremP =
P.locale_target -- Scan.optional (P.opt_thm_name ":" --|
Scan.ahead (P.locale_keyword || P.$$$ "shows")) ("", []) --
general_statement >> (fn ((locale, a), (elems, concl)) =>
fst a) (* a : (bstring * Args.src list) *)
val nameP = P.locale_target |-- (Scan.optional ((P.opt_thm_name ":") >> #1) "")
(* TODO: add preference values for attributes
val prefval = XML.element "prefval" [("name","thm-kind"),("value",name)]
*)
in
(thmnamed_item_elt toks str "opengoal" nameP "") @
(empty "openblock")
end
fun xmls_of_qed (name,markup) = (case name of
"sorry" => markup "giveupgoal"
| "oops" => markup "postponegoal"
| "done" => markup "closegoal"
| "by" => markup "closegoal" (* nested or toplevel *)
| "qed" => markup "closegoal" (* nested or toplevel *)
| "." => markup "closegoal" (* nested or toplevel *)
| ".." => markup "closegoal" (* nested or toplevel *)
| other => (* default to closegoal: may be wrong for extns *)
(parse_warning ("Unrecognized qed command: " ^ quote other); markup "closegoal"))
@ (empty "closeblock")
fun xmls_of_kind kind (name,toks,str) =
let val markup = markup_text str in
case kind of
"control" => markup "badcmd"
| "diag" => markup "spuriouscmd"
(* theory/files *)
| "theory-begin" => xmls_of_thy_begin (name,toks,str)
| "theory-decl" => xmls_of_thy_decl (name,toks,str)
| "theory-heading" => markup "litcomment"
| "theory-script" => markup "theorystep"
| "theory-end" => markup "closetheory"
(* proof control *)
| "theory-goal" => xmls_of_thy_goal (name,toks,str)
| "proof-heading" => markup "litcomment"
| "proof-goal" => (markup "opengoal") @ (empty "openblock") (* nested proof: have, show, ... *)
| "proof-block" => markup "proofstep" (* context-shift: proof, next; really "newgoal" *)
| "proof-open" => (empty "openblock") @ (markup "proofstep")
| "proof-close" => (markup "proofstep") @ (empty "closeblock")
| "proof-script" => markup "proofstep"
| "proof-chain" => markup "proofstep"
| "proof-decl" => markup "proofstep"
| "proof-asm" => markup "proofstep"
| "proof-asm-goal" => (markup "opengoal") @ (empty "openblock") (* nested proof: obtain *)
| "qed" => xmls_of_qed (name,markup)
| "qed-block" => xmls_of_qed (name,markup)
| "qed-global" => xmls_of_qed (name,markup)
| other => (* default for anything else is "spuriouscmd", ignored for undo. *)
(parse_warning ("Internal inconsistency, unrecognized keyword kind: " ^ quote other);
markup "spuriouscmd")
end
in
fun xmls_of_transition (name,str,toks) =
let
val classification = Symtab.lookup (get_keywords_classification_table(),name)
in case classification of
Some k => (xmls_of_kind k (name,toks,str))
| None => (* an uncategorized keyword ignored for undo (maybe wrong) *)
(parse_warning ("Uncategorized command found: " ^ name ^ " -- using spuriouscmd");
markup_text str "spuriouscmd")
end
fun markup_toks [] _ = []
| markup_toks toks x = markup_text (implode (map OuterLex.unparse toks)) x
fun markup_comment_whs [] = []
| markup_comment_whs (toks as t::ts) = (* this would be a lot neater if we could match on toks! *)
let
val (prewhs,rest) = take_prefix (OuterLex.is_kind OuterLex.Space) toks
in
if (prewhs <> []) then
whitespace (implode (map OuterLex.unparse prewhs))
:: (markup_comment_whs rest)
else
(markup_text (OuterLex.unparse t) "comment") @
(markup_comment_whs ts)
end
fun xmls_pre_cmd [] = ([],[])
| xmls_pre_cmd toks =
let
(* an extra token is needed to terminate the command *)
val sync = OuterSyntax.scan "\\<^sync>";
val spaceP = Scan.bulk (Scan.one (fn t =>not (OuterLex.is_proper t)) >> OuterLex.val_of) >> implode
val text_with_whs =
((spaceP || Scan.succeed "") --
(P.short_ident || P.long_ident || P.sym_ident || P.string || P.number || P.verbatim) >> op^)
-- (spaceP || Scan.succeed "") >> op^
val (prewhs,rest1) = take_prefix (not o OuterLex.is_proper) (toks@sync)
(* NB: this collapses litcomment,(litcomment|whitespace)* to a single litcomment *)
val (_,rest2) = (Scan.bulk (P.$$$ "--" |-- text_with_whs) >> implode || Scan.succeed "") rest1
val (postwhs,rest3) = take_prefix (not o OuterLex.is_proper) rest2
in
((markup_comment_whs prewhs) @
(if (length rest2 = length rest1) then []
else markup_text (implode
(map OuterLex.unparse (take (length rest1 - length rest2, rest1))))
"litcomment") @
(markup_comment_whs postwhs),
take (length rest3 - 1,rest3))
end
fun xmls_of_impropers toks =
let
val (xmls,rest) = xmls_pre_cmd toks
in
xmls @ (markup_toks rest "unparseable")
end
fun markup_unparseable str = markup_text str "unparseable"
end
local
(* we have to weave together the whitespace/comments with proper tokens
to reconstruct the input. *)
(* TODO: see if duplicating isar_output/parse_thy can help here *)
fun match_tokens ([],us,vs) = (rev vs,us) (* used, unused *)
| match_tokens (t::ts,w::ws,vs) =
if (t = w) then match_tokens (ts,ws,w::vs)
else match_tokens (t::ts,ws,w::vs)
| match_tokens _ = error ("match_tokens: mismatched input parse")
in
fun xmls_of_str str =
let
(* parsing: See outer_syntax.ML/toplevel_source *)
fun parse_loop ([],[],xmls) = xmls
| parse_loop ([],itoks,xmls) = xmls @ (xmls_of_impropers itoks)
| parse_loop ((nm,toks,_)::trs,itoks,xmls) =
let
(* first proper token after whitespace/litcomment/whitespace is command *)
val (xmls_pre_cmd,cmditoks') = xmls_pre_cmd itoks
val (cmdtok,itoks') = case cmditoks' of x::xs => (x,xs)
| _ => error("proof_general/parse_loop impossible")
val (utoks,itoks'') = match_tokens (toks,itoks',[])
(* FIXME: should take trailing [w/s+] semicolon too in utoks *)
val str = implode (map OuterLex.unparse (cmdtok::utoks))
val xmls_tr = xmls_of_transition (nm,str,toks)
in
parse_loop(trs,itoks'',xmls @ xmls_pre_cmd @ xmls_tr)
end
in
(let val toks = OuterSyntax.scan str
in
parse_loop (OuterSyntax.read toks, toks, [])
end)
handle _ => markup_unparseable str
end
fun parsescript str attrs =
let
val _ = start_delay_msgs () (* accumulate error messages to put inside parseresult *)
val xmls = xmls_of_str str
val errs = end_delayed_msgs ()
in
issue_pgips [XML.element "parseresult" attrs (errs@xmls)]
end
end
(**** PGIP: Isabelle -> Interface ****)
val isabelle_pgml_version_supported = "1.0";
val isabelle_pgip_version_supported = "2.0"
fun usespgip () =
issue_pgipe "usespgip" [("version", isabelle_pgip_version_supported)];
fun usespgml () =
issue_pgipe "usespgml" [("version", isabelle_pgml_version_supported)];
fun hasprefs () =
seq (fn (prefcat, prefs) =>
issue_pgips [XML.element "hasprefs" [("prefcategory",prefcat)]
(map (fn (name, (descr, (ty, (default,_),_))) =>
XML.element "haspref" [("name", name),
("descr", descr),
("default", default)]
[ty]) prefs)]) (!preferences);
fun allprefs () = foldl (op @) ([], map snd (!preferences))
fun setpref name value =
(case assoc (allprefs(), name) of
None => warning ("Unknown pref: " ^ quote name)
| Some (_, (_, _, set)) => set value);
fun getpref name =
(case assoc (allprefs(), name) of
None => warning ("Unknown pref: " ^ quote name)
| Some (_, (_, (_,get), _)) =>
issue_pgip "prefval" [("name", name)] (get ()));
(**** PGIP: Interface -> Isabelle/Isar ****)
exception PGIP of string;
exception PGIP_QUIT;
(* Sending commands to Isar *)
fun isarcmd s =
s |> OuterSyntax.scan |> OuterSyntax.read
|> map (Toplevel.position (Position.name "PGIP message") o #3) |> Toplevel.>>>;
fun xmltext ((XML.Text text)::ts) = text ^ (xmltext ts)
| xmltext [] = ""
| xmltext _ = raise PGIP "Expected text (PCDATA/CDATA)"
fun isarscript xmls = isarcmd (xmltext xmls) (* send a script command *)
(* load an arbitrary (.thy or .ML) file *)
fun use_thy_or_ml_file file =
let
val (path,extn) = Path.split_ext (Path.unpack file)
in
case extn of
"" => isarcmd ("use_thy " ^ (quote (Path.pack path)))
| "thy" => isarcmd ("use_thy " ^ (quote (Path.pack path)))
| "ML" => isarcmd ("use " ^ quote file)
(* instead of error we could guess theory? *)
| other => error ("Don't know how to read a file with extension " ^ other)
end
(* Proof control commands *)
local
fun xmlattro attr attrs = assoc(attrs,attr)
fun xmlattr attr attrs =
(case xmlattro attr attrs of
Some value => value
| None => raise PGIP ("Missing attribute: " ^ attr))
val thyname_attro = xmlattro "thyname"
val thyname_attr = xmlattr "thyname"
val objtype_attro = xmlattro "objtype"
val objtype_attr = xmlattr "objtype"
val name_attr = xmlattr "name"
val dirname_attr = xmlattr "dir"
fun comment x = "(* " ^ x ^ " *)"
fun localfile_of_url url = (* only handle file:/// or file://localhost/ *)
case Url.unpack url of
(Url.File path) => File.sysify_path path
| _ => error ("Cannot access non-local URL " ^ url)
val fileurl_of = localfile_of_url o (xmlattr "url")
val topthy = Toplevel.theory_of o Toplevel.get_state
val topthy_name = PureThy.get_name o topthy
val currently_open_file = ref (None : string option)
in
fun process_pgip_element pgipxml = (case pgipxml of
(XML.Text t) => warning ("Ignored text in PGIP packet: \n" ^ t)
| (xml as (XML.Elem (elem, attrs, data))) =>
(case elem of
(* protocol config *)
"askpgip" => (pgip_emacs_compatibility_flag:=false; (* PG>=3.6 or other PGIP interface *)
usespgip (); send_pgip_config ())
| "askpgml" => usespgml ()
(* proverconfig *)
| "askprefs" => hasprefs ()
| "getpref" => getpref (name_attr attrs)
| "setpref" => setpref (name_attr attrs) (xmltext data)
(* provercontrol *)
| "proverinit" => isar_restart ()
| "proverexit" => isarcmd "quit"
| "startquiet" => isarcmd "disable_pr"
| "stopquiet" => isarcmd "enable_pr"
| "pgmlsymbolson" => (print_mode := !print_mode @ ["xsymbols"])
| "pgmlsymbolsoff" => (print_mode := (!print_mode \ "xsymbols"))
(* properproofcmd: proper commands which belong in script *)
(* FIXME: next ten are by Eclipse interface, can be removed in favour of dostep *)
| "opengoal" => isarscript data
| "proofstep" => isarscript data
| "closegoal" => isarscript data
| "giveupgoal" => isarscript data
| "postponegoal" => isarscript data
| "comment" => isarscript data (* NB: should be ignored, but process anyway *)
| "whitespace" => isarscript data (* NB: should be ignored, but process anyway *)
| "litcomment" => isarscript data
| "spuriouscmd" => isarscript data
| "badcmd" => isarscript data
(* improperproofcmd: improper commands which *do not* belong in script *)
| "dostep" => isarscript data
| "undostep" => isarcmd "undos_proof 1"
| "abortgoal" => isarcmd "ProofGeneral.kill_proof"
| "forget" => error "Not implemented"
| "restoregoal" => error "Not implemented" (* could just treat as forget? *)
(* proofctxt: improper commands *)
| "askids" => askids (thyname_attro attrs, objtype_attro attrs)
| "showid" => showid (thyname_attro attrs, objtype_attr attrs, name_attr attrs)
| "parsescript" => parsescript (xmltext data) attrs (* just pass back attrs unchanged *)
| "showproofstate" => isarcmd "pr"
| "showctxt" => isarcmd "print_theory" (* more useful than print_context *)
| "searchtheorems" => isarcmd ("thms_containing " ^ (xmltext data))
| "setlinewidth" => isarcmd ("pretty_setmargin " ^ (xmltext data))
| "viewdoc" => isarcmd ("print_" ^ (xmltext data)) (* FIXME: isatool doc? *)
(* properfilecmd: proper theory-level script commands *)
(* FIXME: next three are sent by Eclipse, can be removed in favour of doitem *)
| "opentheory" => isarscript data
| "theoryitem" => isarscript data
| "closetheory" => let
val thyname = topthy_name()
in (isarscript data;
writeln ("Theory \""^thyname^"\" completed."))
end
(* improperfilecmd: theory-level commands not in script *)
| "doitem" => isarscript data
| "undoitem" => isarcmd "ProofGeneral.undo"
| "aborttheory" => isarcmd ("init_toplevel")
| "retracttheory" => isarcmd ("kill_thy " ^ (quote (thyname_attr attrs)))
| "loadfile" => use_thy_or_ml_file (fileurl_of attrs)
| "openfile" => (inform_file_retracted (fileurl_of attrs);
currently_open_file := Some (fileurl_of attrs))
| "closefile" => (case !currently_open_file of
Some f => (inform_file_processed f;
currently_open_file := None)
| None => raise PGIP ("closefile when no file is open!"))
| "abortfile" => (currently_open_file := None) (* perhaps error for no file open *)
| "changecwd" => ThyLoad.add_path (dirname_attr attrs)
| "systemcmd" => isarscript data
(* unofficial command for debugging *)
| "quitpgip" => raise PGIP_QUIT
| _ => raise PGIP ("Unrecognized PGIP element: " ^ elem)))
fun process_pgip_tree xml =
(pgip_refseq := None;
pgip_refid := None;
(case xml of
XML.Elem ("pgip", attrs, pgips) =>
(let
val class = xmlattr "class" attrs
val _ = (pgip_refseq := xmlattro "seq" attrs;
pgip_refid := xmlattro "id" attrs)
in
if (class = "pa") then
seq process_pgip_element pgips
else
raise PGIP "PGIP packet for me should have class=\"pa\""
end)
| _ => raise PGIP "Invalid PGIP packet received")
handle (PGIP msg) =>
(error (msg ^ "\nPGIP error occured in XML text below:\n" ^
(XML.string_of_tree xml))))
val process_pgip = process_pgip_tree o XML.tree_of_string;
end
(* PGIP loop: process PGIP input only *)
local
exception XML_PARSE
fun loop src : unit =
let
val _ = issue_pgipe "ready" []
val pgipo = (Source.get_single src)
handle e => raise XML_PARSE
in
case pgipo of
None => ()
| Some (pgip,src') =>
((process_pgip_tree pgip); loop src') handle e => handler (e,Some src')
end handle e => handler (e,Some src) (* i.e. error in ready/XML parse *)
and handler (e,srco) =
case (e,srco) of
(XML_PARSE,Some src) =>
(* (!error_fn "Invalid XML input, aborting"; ()) NB: loop OK for tty, but want exit on EOF *)
panic "Invalid XML input, aborting"
| (PGIP_QUIT,_) => ()
| (ERROR,Some src) => loop src (* message already given *)
| (Interrupt,Some src) => (!error_fn "Interrupt during PGIP processing"; loop src)
| (Toplevel.UNDEF,Some src) => (error "No working context defined"; loop src) (* usually *)
| (e,Some src) => (error (Toplevel.exn_message e); loop src)
| (_,None) => ()
in
(* NB: simple tty for now; later might read from other tty-style sources (e.g. sockets). *)
val xmlP = XML.scan_comment_whspc |-- XML.parse_elem >> single
val tty_src = Source.set_prompt "" (Source.source Symbol.stopper xmlP None Source.tty)
val pgip_toplevel = loop
end
(* additional outer syntax for Isar *)
local structure P = OuterParse and K = OuterSyntax.Keyword in
val undoP = (* undo without output *)
OuterSyntax.improper_command "ProofGeneral.undo" "(internal)" K.control
(Scan.succeed (Toplevel.no_timing o IsarCmd.undo));
val context_thy_onlyP =
OuterSyntax.improper_command "ProofGeneral.context_thy_only" "(internal)" K.control
(P.name >> (Toplevel.no_timing oo IsarThy.init_context update_thy_only));
val try_context_thy_onlyP =
OuterSyntax.improper_command "ProofGeneral.try_context_thy_only" "(internal)" K.control
(P.name >> (Toplevel.no_timing oo
(Toplevel.imperative (K ()) oo IsarThy.init_context try_update_thy_only)));
val restartP =
OuterSyntax.improper_command "ProofGeneral.restart" "(internal)" K.control
(P.opt_unit >> (Toplevel.no_timing oo K (Toplevel.imperative isar_restart)));
val kill_proofP =
OuterSyntax.improper_command "ProofGeneral.kill_proof" "(internal)" K.control
(Scan.succeed (Toplevel.no_timing o IsarCmd.kill_proof_notify tell_clear_goals));
val inform_file_processedP =
OuterSyntax.improper_command "ProofGeneral.inform_file_processed" "(internal)" K.control
(P.name >> (fn file => Toplevel.no_timing o
Toplevel.keep (vacuous_inform_file_processed file) o
Toplevel.kill o
Toplevel.keep (proper_inform_file_processed file)));
val inform_file_retractedP =
OuterSyntax.improper_command "ProofGeneral.inform_file_retracted" "(internal)" K.control
(P.name >> (Toplevel.no_timing oo
(fn file => Toplevel.imperative (fn () => inform_file_retracted file))));
val process_pgipP =
OuterSyntax.improper_command "ProofGeneral.process_pgip" "(internal)" K.control
(P.text >> (Toplevel.no_timing oo
(fn txt => Toplevel.imperative (fn () => process_pgip txt))));
fun init_outer_syntax () = OuterSyntax.add_parsers
[undoP, restartP, kill_proofP, context_thy_onlyP, try_context_thy_onlyP,
inform_file_processedP, inform_file_retractedP, process_pgipP];
end;
(* init *)
val initialized = ref false;
fun set_prompts true _ = ml_prompts "ML> " "ML# "
| set_prompts false true = ml_prompts "PGIP-ML>" "PGIP-ML# "
| set_prompts false false =
ml_prompts ("> " ^ oct_char "372") ("- " ^ oct_char "373");
fun init_setup isar pgip =
(conditional (not (! initialized)) (fn () =>
(if isar then setmp warning_fn (K ()) init_outer_syntax () else ();
setup_xsymbols_output ();
setup_pgml_output ();
setup_messages ();
setup_state ();
setup_thy_loader ();
setup_present_hook ();
set initialized; ()));
sync_thy_loader ();
print_mode := proof_generalN :: (! print_mode \ proof_generalN);
if pgip then
print_mode := pgmlN :: (pgmlatomsN :: (! print_mode \ pgmlN \ pgmlatomsN))
else
pgip_emacs_compatibility_flag := true; (* assume this for PG <3.6 compatibility *)
set quick_and_dirty;
ThmDeps.enable ();
set_prompts isar pgip;
pgip_active := pgip)
fun init isar =
(init_setup isar false;
if isar then ((* da: this welcome is problematic: clashes with welcome
issued for PG anyway.
welcome (); *)
Isar.sync_main ()) else isa_restart ());
fun init_pgip false = panic "Sorry, PGIP not supported for Isabelle/classic mode."
| init_pgip true = (init_setup true true;
pgip_toplevel tty_src);
(** generate keyword classification elisp file **)
local
val regexp_meta = explode ".*+?[]^$";
val regexp_quote =
implode o map (fn c => if c mem regexp_meta then "\\\\" ^ c else c)
o explode;
fun defconst name strs =
"\n(defconst isar-keywords-" ^ name ^
"\n '(" ^ space_implode "\n " (map (quote o regexp_quote) strs) ^ "))\n";
fun make_elisp_commands commands kind =
defconst kind (mapfilter
(fn (c, _, k, _) => if k = kind then Some c else None)
commands);
fun make_elisp_syntax (keywords, commands) =
";;\n\
\;; Keyword classification tables for Isabelle/Isar.\n\
\;; This file was generated by " ^ Session.name () ^ " -- DO NOT EDIT!\n\
\;;\n\
\;; $" ^ "Id$\n\
\;;\n" ^
defconst "major" (map #1 commands) ^
defconst "minor" (filter Syntax.is_identifier keywords) ^
implode (map (make_elisp_commands commands) OuterSyntax.Keyword.kinds) ^
"\n(provide 'isar-keywords)\n";
in
fun write_keywords s =
(init_outer_syntax ();
File.write (Path.unpack ("isar-keywords" ^ (if s = "" then "" else "-" ^ s) ^".el"))
(make_elisp_syntax (OuterSyntax.dest_keywords (),
OuterSyntax.dest_parsers ())));
end;
end