--- a/src/Pure/Syntax/syntax_phases.ML Sun Nov 25 18:50:13 2012 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML Sun Nov 25 19:49:24 2012 +0100
@@ -51,16 +51,16 @@
[Name_Space.markup (Consts.space_of (Proof_Context.consts_of ctxt)) c];
fun markup_free ctxt x =
- [if can Name.dest_skolem x then Isabelle_Markup.skolem else Isabelle_Markup.free] @
+ [if can Name.dest_skolem x then Markup.skolem else Markup.free] @
(if Variable.is_body ctxt orelse Variable.is_fixed ctxt x
then [Variable.markup_fixed ctxt x]
else []);
-fun markup_var xi = [Markup.name (Term.string_of_vname xi) Isabelle_Markup.var];
+fun markup_var xi = [Markup.name (Term.string_of_vname xi) Markup.var];
fun markup_bound def ps (name, id) =
- let val entity = Isabelle_Markup.entity Isabelle_Markup.boundN name in
- Isabelle_Markup.bound ::
+ let val entity = Markup.entity Markup.boundN name in
+ Markup.bound ::
map (fn pos => Markup.properties (Position.entity_properties_of def id pos) entity) ps
end;
@@ -298,8 +298,7 @@
val pts = Syntax.parse syn root (filter Lexicon.is_proper toks)
handle ERROR msg =>
error (msg ^
- implode
- (map (Markup.markup Isabelle_Markup.report o Lexicon.reported_token_range ctxt) toks));
+ implode (map (Markup.markup Markup.report o Lexicon.reported_token_range ctxt) toks));
val len = length pts;
val limit = Config.get ctxt Syntax.ambiguity_limit;
@@ -330,11 +329,10 @@
fun parse_failed ctxt pos msg kind =
cat_error msg ("Failed to parse " ^ kind ^
- Markup.markup Isabelle_Markup.report
- (Context_Position.reported_text ctxt pos Isabelle_Markup.bad ""));
+ Markup.markup Markup.report (Context_Position.reported_text ctxt pos Markup.bad ""));
fun parse_sort ctxt =
- Syntax.parse_token ctxt Term_XML.Decode.sort Isabelle_Markup.sort
+ Syntax.parse_token ctxt Term_XML.Decode.sort Markup.sort
(fn (syms, pos) =>
parse_tree ctxt "sort" (syms, pos)
|> uncurry (report_result ctxt pos)
@@ -343,7 +341,7 @@
handle ERROR msg => parse_failed ctxt pos msg "sort");
fun parse_typ ctxt =
- Syntax.parse_token ctxt Term_XML.Decode.typ Isabelle_Markup.typ
+ Syntax.parse_token ctxt Term_XML.Decode.typ Markup.typ
(fn (syms, pos) =>
parse_tree ctxt "type" (syms, pos)
|> uncurry (report_result ctxt pos)
@@ -354,8 +352,8 @@
let
val (markup, kind, root, constrain) =
if is_prop
- then (Isabelle_Markup.prop, "proposition", "prop", Type.constraint propT)
- else (Isabelle_Markup.term, "term", Config.get ctxt Syntax.root, I);
+ then (Markup.prop, "proposition", "prop", Type.constraint propT)
+ else (Markup.term, "term", Config.get ctxt Syntax.root, I);
val decode = constrain o Term_XML.Decode.term;
in
Syntax.parse_token ctxt decode markup
@@ -605,24 +603,23 @@
let
val m =
if Variable.is_fixed ctxt x orelse Syntax.is_pretty_global ctxt
- then Isabelle_Markup.fixed x
- else Isabelle_Markup.intensify;
+ then Markup.fixed x else Markup.intensify;
in
if can Name.dest_skolem x
- then ([m, Isabelle_Markup.skolem], Variable.revert_fixed ctxt x)
- else ([m, Isabelle_Markup.free], x)
+ then ([m, Markup.skolem], Variable.revert_fixed ctxt x)
+ else ([m, Markup.free], x)
end;
fun var_or_skolem s =
(case Lexicon.read_variable s of
SOME (x, i) =>
(case try Name.dest_skolem x of
- NONE => (Isabelle_Markup.var, s)
- | SOME x' => (Isabelle_Markup.skolem, Term.string_of_vname (x', i)))
- | NONE => (Isabelle_Markup.var, s));
+ NONE => (Markup.var, s)
+ | SOME x' => (Markup.skolem, Term.string_of_vname (x', i)))
+ | NONE => (Markup.var, s));
-val typing_elem = YXML.output_markup_elem Isabelle_Markup.typing;
-val sorting_elem = YXML.output_markup_elem Isabelle_Markup.sorting;
+val typing_elem = YXML.output_markup_elem Markup.typing;
+val sorting_elem = YXML.output_markup_elem Markup.sorting;
fun unparse_t t_to_ast prt_t markup ctxt t =
let
@@ -647,14 +644,14 @@
case_fixed = fn x => free_or_skolem ctxt x,
case_default = fn x => ([], x)});
- fun token_trans "_tfree" x = SOME (Pretty.mark_str (Isabelle_Markup.tfree, x))
- | token_trans "_tvar" x = SOME (Pretty.mark_str (Isabelle_Markup.tvar, x))
+ fun token_trans "_tfree" x = SOME (Pretty.mark_str (Markup.tfree, x))
+ | token_trans "_tvar" x = SOME (Pretty.mark_str (Markup.tvar, x))
| token_trans "_free" x = SOME (Pretty.marks_str (free_or_skolem ctxt x))
- | token_trans "_bound" x = SOME (Pretty.mark_str (Isabelle_Markup.bound, x))
- | token_trans "_loose" x = SOME (Pretty.mark_str (Isabelle_Markup.bad, x))
+ | token_trans "_bound" x = SOME (Pretty.mark_str (Markup.bound, x))
+ | token_trans "_loose" x = SOME (Pretty.mark_str (Markup.bad, x))
| token_trans "_var" x = SOME (Pretty.mark_str (var_or_skolem x))
- | token_trans "_numeral" x = SOME (Pretty.mark_str (Isabelle_Markup.numeral, x))
- | token_trans "_inner_string" x = SOME (Pretty.mark_str (Isabelle_Markup.inner_string, x))
+ | token_trans "_numeral" x = SOME (Pretty.mark_str (Markup.numeral, x))
+ | token_trans "_inner_string" x = SOME (Pretty.mark_str (Markup.inner_string, x))
| token_trans _ _ = NONE;
fun markup_trans a [Ast.Variable x] = token_trans a x
@@ -694,8 +691,8 @@
in
-val unparse_sort = unparse_t sort_to_ast Printer.pretty_typ_ast Isabelle_Markup.sort;
-val unparse_typ = unparse_t typ_to_ast Printer.pretty_typ_ast Isabelle_Markup.typ;
+val unparse_sort = unparse_t sort_to_ast Printer.pretty_typ_ast Markup.sort;
+val unparse_typ = unparse_t typ_to_ast Printer.pretty_typ_ast Markup.typ;
fun unparse_term ctxt =
let
@@ -705,7 +702,7 @@
in
unparse_t (term_to_ast idents (is_some o Syntax.lookup_const syn))
(Printer.pretty_term_ast (not (Pure_Thy.old_appl_syntax thy)))
- Isabelle_Markup.term ctxt
+ Markup.term ctxt
end;
end;
@@ -871,7 +868,7 @@
val typing_report =
fold2 (fn (pos, _) => fn ty =>
if Position.is_reported pos then
- cons (Position.reported_text pos Isabelle_Markup.typing
+ cons (Position.reported_text pos Markup.typing
(Syntax.string_of_typ ctxt (Logic.dest_type ty)))
else I) ps tys' []
|> implode;