# HG changeset patch
# User wenzelm
# Date 1349980682 -7200
# Node ID d15fe10593ff52c842efe4f6a0293682d58b5217
# Parent  f7a1e1745b7b2f0cb9797f6568f748981a6bf54b
clarified output token markup (see also bc22daeed49e);

diff -r f7a1e1745b7b -r d15fe10593ff src/Pure/Syntax/lexicon.ML
--- 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 =
diff -r f7a1e1745b7b -r d15fe10593ff src/Pure/Syntax/printer.ML
--- 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)