--- a/src/Pure/ProofGeneral/proof_general_emacs.ML Thu Apr 17 16:30:51 2008 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Thu Apr 17 16:30:52 2008 +0200
@@ -53,70 +53,27 @@
end;
-(* token translations *)
-
-local
-
-fun end_tag () = special "350";
-val class_tag = ("class", fn () => special "351");
-val tfree_tag = ("tfree", fn () => special "352");
-val tvar_tag = ("tvar", fn () => special "353");
-val free_tag = ("free", fn () => special "354");
-val bound_tag = ("bound", fn () => special "355");
-val var_tag = ("var", fn () => special "356");
-val skolem_tag = ("skolem", fn () => special "357");
-
-fun xml_atom kind x = XML.element "atom" [("kind", kind)] [XML.text x];
-
-fun tagit (kind, bg_tag) x =
- (bg_tag () ^ x ^ end_tag (), Symbol.length (Symbol.explode x));
-
-fun free_or_skolem x =
- (case try Name.dest_skolem x of
- NONE => tagit free_tag x
- | SOME x' => tagit skolem_tag x');
-
-fun var_or_skolem s =
- (case Lexicon.read_variable s of
- SOME (x, i) =>
- (case try Name.dest_skolem x of
- NONE => tagit var_tag s
- | SOME x' => tagit skolem_tag
- (setmp show_question_marks true Term.string_of_vname (x', i)))
- | NONE => 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 _ = Context.>> (Context.map_theory (Sign.add_tokentrfuns proof_general_trans));
-
-end;
-
-
(* common markup *)
-fun proof_general_markup (name, props) =
+val _ = Markup.add_mode proof_generalN (fn (name, props) =>
let
val (bg1, en1) =
if name = Markup.stateN then (special "366" ^ "\n", "\n" ^ special "367")
else if name = Markup.sendbackN then (special "376", special "377")
else if name = Markup.hiliteN then (special "327", special "330")
+ else if name = Markup.classN then (special "351", special "350")
+ else if name = Markup.tfreeN then (special "352", special "350")
+ else if name = Markup.tvarN then (special "353", special "350")
+ else if name = Markup.freeN then (special "354", special "350")
+ else if name = Markup.boundN then (special "355", special "350")
+ else if name = Markup.varN then (special "356", special "350")
+ else if name = Markup.skolemN then (special "357", special "350")
else ("", "");
val (bg2, en2) =
if print_mode_active test_markupN
then XML.output_markup (name, props)
else ("", "");
- in (bg1 ^ bg2, en2 ^ en1) end;
-
-val _ = Markup.add_mode proof_generalN proof_general_markup;
+ in (bg1 ^ bg2, en2 ^ en1) end);
(* messages and notification *)
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML Thu Apr 17 16:30:51 2008 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Thu Apr 17 16:30:52 2008 +0200
@@ -44,7 +44,7 @@
fun pgml_sym s =
(case Symbol.decode s of
Symbol.Char s => XML.text s
- | Symbol.Sym sn =>
+ | Symbol.Sym sn =>
let val ascii = implode (map xsym_output (Symbol.explode s))
in if !pgmlsymbols_flag then XML.element "sym" [("name", sn)] [XML.text ascii]
else ascii end
@@ -63,53 +63,6 @@
end;
-(* token translations *)
-
-local
-
-val class_tag = "class"
-val tfree_tag = "tfree"
-val tvar_tag = "tvar"
-val free_tag = "free"
-val bound_tag = "bound"
-val var_tag = "var"
-val skolem_tag = "skolem"
-
-fun xml_atom kind x = XML.element "atom" [("kind", kind)] [XML.text x];
-
-fun tagit kind x =
- (xml_atom kind x, Symbol.length (Symbol.explode x));
-
-fun free_or_skolem x =
- (case try Name.dest_skolem x of
- NONE => tagit free_tag x
- | SOME x' => tagit skolem_tag x');
-
-fun var_or_skolem s =
- (case Lexicon.read_variable s of
- SOME (x, i) =>
- (case try Name.dest_skolem x of
- NONE => tagit var_tag s
- | SOME x' => tagit skolem_tag
- (setmp show_question_marks true Term.string_of_vname (x', i)))
- | NONE => 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 _ = Context.>> (Context.map_theory (Sign.add_tokentrfuns proof_general_trans));
-
-end;
-
-
(* assembling and issuing PGIP packets *)
val pgip_refid = ref NONE: string option ref;
@@ -146,10 +99,10 @@
val output_pgips =
XML.string_of o PgipOutput.output o assemble_pgips o map PgipOutput.output;
-val output_pgmlterm =
+val output_pgmlterm =
XML.string_of o Pgml.pgmlterm_to_xml;
-val output_pgmltext =
+val output_pgmltext =
XML.string_of o Pgml.pgml_to_xml;
@@ -179,10 +132,10 @@
delayed_msgs := pgip :: ! delayed_msgs
else issue_pgip pgip
- fun wrap_pgml area s =
- if String.isPrefix "<pgml" s then
+ fun wrap_pgml area s =
+ if String.isPrefix "<pgml" s then
XML.Output s (* already pgml outermost *)
- else
+ else
Pgml.pgml_to_xml (pgml area [Pgml.Raw (XML.Output s)]) (* mixed *)
in
@@ -242,9 +195,9 @@
(* immediate messages *)
-fun tell_clear_goals () =
+fun tell_clear_goals () =
issue_pgip (Normalresponse { content = [Pgml.pgml_to_xml (pgml Display [])] })
-fun tell_clear_response () =
+fun tell_clear_response () =
issue_pgip (Normalresponse { content = [Pgml.pgml_to_xml (pgml Message [])] })
fun tell_file_loaded completed path =
@@ -273,46 +226,39 @@
fun block_markup markup =
- let
- val pgml = Pgml.Box { orient = NONE,
+ let
+ val pgml = Pgml.Box { orient = NONE,
indent = Markup.get_int markup Markup.indentN,
content = pgmlterms_no_text }
in split_markup (output_pgmlterm pgml) end;
fun break_markup markup =
- let
+ let
val pgml = Pgml.Break { mandatory = NONE,
indent = Markup.get_int markup Markup.widthN }
in (output_pgmlterm pgml, "") end;
fun fbreak_markup markup =
- let
+ let
val pgml = Pgml.Break { mandatory = SOME true, indent = NONE }
in (output_pgmlterm pgml, "") end;
val state_markup =
split_markup (output_pgmltext (pgml PgipTypes.Display pgmlterms_no_text))
-fun proof_general_markup (markup as (name, _)) =
- if name = Markup.blockN then block_markup markup
- else if name = Markup.breakN then break_markup markup
- else if name = Markup.fbreakN then fbreak_markup markup
-(* else if name = Markup.classN then class_markup markup
- else if name = Markup.tyconN then tycon_markup markup
- else if name = Markup.constN then const_markup markup
- else if name = Markup.axiomN then axiom_markup markup
- else if name = Markup.sortN then sort_markup markup
- else if name = Markup.typN then typ_markup markup
- else if name = Markup.termN then term_markup markup
- else if name = Markup.keywordN then keyword_markup markup
- else if name = Markup.commandN then command_markup markup*)
- else if name = Markup.stateN then state_markup
-(* else if name = Markup.subgoalN then subgoal_markup () *)
- else ("", "");
+val token_markups =
+ [Markup.classN, Markup.tfreeN, Markup.tvarN, Markup.freeN,
+ Markup.boundN, Markup.varN, Markup.skolemN];
in
-val _ = Markup.add_mode proof_generalN proof_general_markup;
+val _ = Markup.add_mode proof_generalN (fn (markup as (name, _)) =>
+ if name = Markup.blockN then block_markup markup
+ else if name = Markup.breakN then break_markup markup
+ else if name = Markup.fbreakN then fbreak_markup markup
+ else if name = Markup.stateN then state_markup
+ else if member (op =) token_markups name then XML.output_markup ("atom", [("kind", name)])
+ else ("", ""));
end;
@@ -562,13 +508,13 @@
fun proverexit _ = isarcmd "quit"
-fun set_proverflag_quiet b =
+fun set_proverflag_quiet b =
isarcmd (if b then "disable_pr" else "enable_pr")
fun set_proverflag_pgmlsymbols b =
(pgmlsymbols_flag := b;
NAMED_CRITICAL "print_mode" (fn () =>
- change print_mode
+ change print_mode
(fn mode =>
remove (op =) Symbol.xsymbolsN mode @ (if b then [Symbol.xsymbolsN] else []))))
@@ -577,17 +523,17 @@
Proofterm.proofs := (if b then 1 else 2))
fun setproverflag (Setproverflag vs) =
- let
+ let
val flagname = #flagname vs
val value = #value vs
in
(case flagname of
"quiet" => set_proverflag_quiet value
| "pgmlsymbols" => set_proverflag_pgmlsymbols value
- | "metainfo:thmdeps" => set_proverflag_thmdeps value
- | _ => log_msg ("Unrecognised prover control flag: " ^
+ | "metainfo:thmdeps" => set_proverflag_thmdeps value
+ | _ => log_msg ("Unrecognised prover control flag: " ^
(quote flagname) ^ " ignored."))
- end
+ end
fun dostep (Dostep vs) =
@@ -643,13 +589,13 @@
| SOME prf => filter (String.isPrefix (unprefix (prf ^ NameSpace.separator) thy))
(thms_of_thy prf))
val qualified_thms_of_thy = (* for global query with single response *)
- (map fst) o NameSpace.dest_table o PureThy.theorems_of o ThyInfo.get_theory;
+ (map fst) o NameSpace.dest_table o PureThy.theorems_of o ThyInfo.get_theory;
(* da: this version is equivalent to my previous, but splits up theorem sets with names
that I can't get to access later with get_thm. Anyway, would rather use sets.
Is above right way to get qualified names in that case? Filtering required again?
map PureThy.get_name_hint o filter PureThy.has_name_hint o
map snd o PureThy.thms_of o ThyInfo.get_theory; *)
- in
+ in
case (thyname,objtype) of
(NONE, NONE) =>
setids (idtable ObjFile NONE (ThyInfo.get_names())) (*FIXME: uris*)
@@ -743,11 +689,11 @@
(thy::(rest as _::_)) => (ThyInfo.get_theory thy, space_implode "." rest)
| [plainid] => (topthy(),plainid)
| _ => raise Toplevel.UNDEF (* assert false *)
- end
-
+ end
+
fun idvalue strings =
- issue_pgip (Idvalue { thyname=thyname, objtype=objtype, name=name,
+ issue_pgip (Idvalue { thyname=thyname, objtype=objtype, name=name,
text=[XML.Elem("pgml",[],
map XML.Output strings)] })
@@ -1169,3 +1115,4 @@
end
end;
+
--- a/src/Pure/Tools/isabelle_process.ML Thu Apr 17 16:30:51 2008 +0200
+++ b/src/Pure/Tools/isabelle_process.ML Thu Apr 17 16:30:52 2008 +0200
@@ -112,43 +112,6 @@
Output.prompt_fn := message "G");
-(* token translations *)
-
-local
-
-fun markup kind x =
- ((YXML.output_markup (kind, []) |-> enclose) (Output.output x), Symbol.length (Symbol.explode x));
-
-fun free_or_skolem x =
- (case try Name.dest_skolem x of
- NONE => markup Markup.freeN x
- | SOME x' => markup Markup.skolemN x');
-
-fun var_or_skolem s =
- (case Lexicon.read_variable s of
- SOME (x, i) =>
- (case try Name.dest_skolem x of
- NONE => markup Markup.varN s
- | SOME x' => markup Markup.skolemN
- (setmp show_question_marks true Term.string_of_vname (x', i)))
- | NONE => markup Markup.varN s);
-
-val token_trans =
- Syntax.tokentrans_mode full_markupN
- [("class", markup Markup.classN),
- ("tfree", markup Markup.tfreeN),
- ("tvar", markup Markup.tvarN),
- ("free", free_or_skolem),
- ("bound", markup Markup.boundN),
- ("var", var_or_skolem)];
-
-in
-
-val _ = Context.>> (Context.map_theory (Sign.add_tokentrfuns token_trans));
-
-end;
-
-
(* init *)
fun init () =