--- a/src/Pure/Syntax/syntax_phases.ML Sat Mar 01 19:55:01 2014 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML Sat Mar 01 22:46:31 2014 +0100
@@ -440,7 +440,8 @@
else decode_appl ps asts
| decode ps (Ast.Appl asts) = decode_appl ps asts;
- val (syms, pos) = Syntax.read_token str;
+ val {text, pos, ...} = Syntax.read_token_source str;
+ val syms = Symbol_Pos.explode (text, pos);
val ast =
parse_asts ctxt true root (syms, pos)
|> uncurry (report_result ctxt pos)
@@ -749,8 +750,8 @@
in
-val unparse_sort = unparse_t sort_to_ast Printer.pretty_typ_ast Markup.language_sort;
-val unparse_typ = unparse_t typ_to_ast Printer.pretty_typ_ast Markup.language_type;
+val unparse_sort = unparse_t sort_to_ast Printer.pretty_typ_ast (Markup.language_sort false);
+val unparse_typ = unparse_t typ_to_ast Printer.pretty_typ_ast (Markup.language_type false);
fun unparse_term ctxt =
let
@@ -760,7 +761,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)))
- Markup.language_term ctxt
+ (Markup.language_term false) ctxt
end;
end;