--- a/src/Pure/Syntax/lexicon.ML Thu Oct 11 19:25:36 2012 +0200
+++ b/src/Pure/Syntax/lexicon.ML Thu Oct 11 20:38:02 2012 +0200
@@ -44,6 +44,7 @@
val tvarT: typ
val terminals: string list
val is_terminal: string -> bool
+ val literal_markup: string -> Markup.T
val report_of_token: token -> Position.report
val reported_token_range: Proof.context -> token -> string
val matching_tokens: token * token -> bool
@@ -188,25 +189,24 @@
(* markup *)
+fun literal_markup s =
+ if is_ascii_identifier s
+ then Isabelle_Markup.literal
+ else Isabelle_Markup.delimiter;
+
val token_kind_markup =
- fn Literal => Isabelle_Markup.literal
- | IdentSy => Markup.empty
- | LongIdentSy => Markup.empty
- | VarSy => Isabelle_Markup.var
- | TFreeSy => Isabelle_Markup.tfree
- | TVarSy => Isabelle_Markup.tvar
- | NumSy => Isabelle_Markup.numeral
- | FloatSy => Isabelle_Markup.numeral
- | XNumSy => Isabelle_Markup.numeral
- | StrSy => Isabelle_Markup.inner_string
- | Space => Markup.empty
- | Comment => Isabelle_Markup.inner_comment
- | EOF => Markup.empty;
+ fn VarSy => Isabelle_Markup.var
+ | TFreeSy => Isabelle_Markup.tfree
+ | TVarSy => Isabelle_Markup.tvar
+ | NumSy => Isabelle_Markup.numeral
+ | FloatSy => Isabelle_Markup.numeral
+ | XNumSy => Isabelle_Markup.numeral
+ | StrSy => Isabelle_Markup.inner_string
+ | Comment => Isabelle_Markup.inner_comment
+ | _ => Markup.empty;
fun report_of_token (Token (kind, s, (pos, _))) =
- let val markup =
- if kind = Literal andalso not (is_ascii_identifier s) then Isabelle_Markup.delimiter
- else token_kind_markup kind
+ let val markup = if kind = Literal then literal_markup s else token_kind_markup kind
in (pos, markup) end;
fun reported_token_range ctxt tok =
--- a/src/Pure/Syntax/printer.ML Thu Oct 11 19:25:36 2012 +0200
+++ b/src/Pure/Syntax/printer.ML Thu Oct 11 20:38:02 2012 +0200
@@ -92,8 +92,7 @@
datatype symb =
Arg of int |
TypArg of int |
- String of string |
- Space of string |
+ String of bool * string |
Break of int |
Block of int * symb list;
@@ -113,11 +112,12 @@
(if Lexicon.is_terminal s then 1000 else p);
fun xsyms_to_syms (Syntax_Ext.Delim s :: xsyms) =
- apfst (cons (String s)) (xsyms_to_syms xsyms)
+ apfst (cons (String (not (exists Symbol.is_block_ctrl (Symbol.explode s)), s)))
+ (xsyms_to_syms xsyms)
| xsyms_to_syms (Syntax_Ext.Argument s_p :: xsyms) =
apfst (cons (arg s_p)) (xsyms_to_syms xsyms)
| xsyms_to_syms (Syntax_Ext.Space s :: xsyms) =
- apfst (cons (Space s)) (xsyms_to_syms xsyms)
+ apfst (cons (String (false, s))) (xsyms_to_syms xsyms)
| xsyms_to_syms (Syntax_Ext.Bg i :: xsyms) =
let
val (bsyms, xsyms') = xsyms_to_syms xsyms;
@@ -133,7 +133,6 @@
fun nargs (Arg _ :: syms) = nargs syms + 1
| nargs (TypArg _ :: syms) = nargs syms + 1
| nargs (String _ :: syms) = nargs syms
- | nargs (Space _ :: syms) = nargs syms
| nargs (Break _ :: syms) = nargs syms
| nargs (Block (_, bsyms) :: syms) = nargs syms + nargs bsyms
| nargs [] = 0;
@@ -202,17 +201,14 @@
(pretty true curried (Config.put pretty_priority p ctxt)
tabs trf markup_trans markup_extern t @ Ts, args')
end
- | synT m (String s :: symbs, args) =
+ | synT m (String (do_mark, s) :: symbs, args) =
let
val (Ts, args') = synT m (symbs, args);
val T =
- if exists Symbol.is_block_ctrl (Symbol.explode s)
- then Pretty.str s
- else Pretty.marks_str (m, s);
+ if do_mark
+ then Pretty.marks_str (m @ [Lexicon.literal_markup s], s)
+ else Pretty.str s;
in (T :: Ts, args') end
- | synT m (Space s :: symbs, args) =
- let val (Ts, args') = synT m (symbs, args);
- in (Pretty.str s :: Ts, args') end
| synT m (Block (i, bsymbs) :: symbs, args) =
let
val (bTs, args') = synT m (bsymbs, args);
@@ -229,7 +225,7 @@
and parT m (pr, args, p, p': int) = #1 (synT m
(if p > p' orelse (show_brackets andalso p' <> 1000 andalso not (is_chain pr))
- then [Block (1, Space "(" :: pr @ [Space ")"])]
+ then [Block (1, String (false, "(") :: pr @ [String (false, ")")])]
else pr, args))
and atomT a = Pretty.marks_str (markup_extern a)