# HG changeset patch
# User wenzelm
# Date 1393344235 -3600
# Node ID 4a4e5686e091f254b20f7edc1a9315bb96df572c
# Parent  225a060e744529689e8c7ddd27516e5617548183
clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
tuned message;

diff -r 225a060e7445 -r 4a4e5686e091 src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Tue Feb 25 14:56:58 2014 +0100
+++ b/src/Pure/Isar/token.ML	Tue Feb 25 17:03:55 2014 +0100
@@ -42,6 +42,7 @@
   val inner_syntax_of: T -> string
   val source_position_of: T -> Symbol_Pos.text * Position.T
   val content_of: T -> string
+  val markup: T -> Markup.T * string
   val unparse: T -> string
   val text_of: T -> string * string
   val get_files: T -> file Exn.result list
@@ -213,6 +214,42 @@
 fun content_of (Token (_, (_, x), _)) = x;
 
 
+(* markup *)
+
+local
+
+val token_kind_markup =
+ fn Command       => (Markup.keyword1, "")
+  | Keyword       => (Markup.keyword2, "")
+  | Ident         => (Markup.empty, "")
+  | LongIdent     => (Markup.empty, "")
+  | SymIdent      => (Markup.empty, "")
+  | Var           => (Markup.var, "")
+  | TypeIdent     => (Markup.tfree, "")
+  | TypeVar       => (Markup.tvar, "")
+  | Nat           => (Markup.empty, "")
+  | Float         => (Markup.empty, "")
+  | String        => (Markup.string, "")
+  | AltString     => (Markup.altstring, "")
+  | Verbatim      => (Markup.verbatim, "")
+  | Cartouche     => (Markup.cartouche, "")
+  | Space         => (Markup.empty, "")
+  | Comment       => (Markup.comment, "")
+  | InternalValue => (Markup.empty, "")
+  | Error msg     => (Markup.bad, msg)
+  | Sync          => (Markup.control, "")
+  | EOF           => (Markup.control, "");
+
+in
+
+fun markup tok =
+  if keyword_with (not o Symbol.is_ascii_identifier) tok
+  then (Markup.operator, "")
+  else token_kind_markup (kind_of tok);
+
+end;
+
+
 (* unparse *)
 
 fun unparse (Token (_, (kind, x), _)) =
@@ -231,11 +268,13 @@
   else
     let
       val k = str_of_kind (kind_of tok);
+      val (m, _) = markup tok;
       val s = unparse tok;
     in
       if s = "" then (k, "")
-      else if size s < 40 andalso not (exists_string (fn c => c = "\n") s) then (k ^ " " ^ s, "")
-      else (k, s)
+      else if size s < 40 andalso not (exists_string (fn c => c = "\n") s)
+      then (k ^ " " ^ Markup.markup m s, "")
+      else (k, Markup.markup m s)
     end;
 
 
diff -r 225a060e7445 -r 4a4e5686e091 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Tue Feb 25 14:56:58 2014 +0100
+++ b/src/Pure/PIDE/markup.ML	Tue Feb 25 17:03:55 2014 +0100
@@ -97,9 +97,8 @@
   val document_antiquotation_optionN: string
   val paragraphN: string val paragraph: T
   val text_foldN: string val text_fold: T
-  val keywordN: string val keyword: T
+  val commandN: string
   val operatorN: string val operator: T
-  val commandN: string val command: T
   val stringN: string val string: T
   val altstringN: string val altstring: T
   val verbatimN: string val verbatim: T
@@ -396,9 +395,11 @@
 
 (* outer syntax *)
 
-val (keywordN, keyword) = markup_elem "keyword";
+val commandN = "command";
+
+val (keyword1N, keyword1) = markup_elem "keyword1";
+val (keyword2N, keyword2) = markup_elem "keyword2";
 val (operatorN, operator) = markup_elem "operator";
-val (commandN, command) = markup_elem "command";
 val (stringN, string) = markup_elem "string";
 val (altstringN, altstring) = markup_elem "altstring";
 val (verbatimN, verbatim) = markup_elem "verbatim";
@@ -409,9 +410,6 @@
 val tokenN = "token";
 fun token props = (tokenN, props);
 
-val (keyword1N, keyword1) = markup_elem "keyword1";
-val (keyword2N, keyword2) = markup_elem "keyword2";
-
 
 (* timing *)
 
diff -r 225a060e7445 -r 4a4e5686e091 src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Tue Feb 25 14:56:58 2014 +0100
+++ b/src/Pure/PIDE/markup.scala	Tue Feb 25 17:03:55 2014 +0100
@@ -209,9 +209,11 @@
 
   /* outer syntax */
 
-  val KEYWORD = "keyword"
+  val COMMAND = "command"
+
+  val KEYWORD1 = "keyword1"
+  val KEYWORD2 = "keyword2"
   val OPERATOR = "operator"
-  val COMMAND = "command"
   val STRING = "string"
   val ALTSTRING = "altstring"
   val VERBATIM = "verbatim"
@@ -219,9 +221,6 @@
   val COMMENT = "comment"
   val CONTROL = "control"
 
-  val KEYWORD1 = "keyword1"
-  val KEYWORD2 = "keyword2"
-
 
   /* timing */
 
diff -r 225a060e7445 -r 4a4e5686e091 src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Tue Feb 25 14:56:58 2014 +0100
+++ b/src/Pure/Thy/latex.ML	Tue Feb 25 17:03:55 2014 +0100
@@ -178,10 +178,8 @@
   in (output_symbols syms, Symbol.length syms) end;
 
 fun latex_markup (s, _) =
-  if s = Markup.commandN orelse s = Markup.keyword1N
-    then ("\\isacommand{", "}")
-  else if s = Markup.keywordN orelse s = Markup.keyword2N
-    then ("\\isakeyword{", "}")
+  if s = Markup.keyword1N then ("\\isacommand{", "}")
+  else if s = Markup.keyword2N then ("\\isakeyword{", "}")
   else Markup.no_output;
 
 fun latex_indent "" _ = ""
diff -r 225a060e7445 -r 4a4e5686e091 src/Pure/Thy/thy_syntax.ML
--- a/src/Pure/Thy/thy_syntax.ML	Tue Feb 25 14:56:58 2014 +0100
+++ b/src/Pure/Thy/thy_syntax.ML	Tue Feb 25 17:03:55 2014 +0100
@@ -42,41 +42,6 @@
 
 local
 
-val token_kind_markup =
- fn Token.Command       => (Markup.command, "")
-  | Token.Keyword       => (Markup.keyword, "")
-  | Token.Ident         => (Markup.empty, "")
-  | Token.LongIdent     => (Markup.empty, "")
-  | Token.SymIdent      => (Markup.empty, "")
-  | Token.Var           => (Markup.var, "")
-  | Token.TypeIdent     => (Markup.tfree, "")
-  | Token.TypeVar       => (Markup.tvar, "")
-  | Token.Nat           => (Markup.empty, "")
-  | Token.Float         => (Markup.empty, "")
-  | Token.String        => (Markup.string, "")
-  | Token.AltString     => (Markup.altstring, "")
-  | Token.Verbatim      => (Markup.verbatim, "")
-  | Token.Cartouche     => (Markup.cartouche, "")
-  | Token.Space         => (Markup.empty, "")
-  | Token.Comment       => (Markup.comment, "")
-  | Token.InternalValue => (Markup.empty, "")
-  | Token.Error msg     => (Markup.bad, msg)
-  | Token.Sync          => (Markup.control, "")
-  | Token.EOF           => (Markup.control, "");
-
-fun token_markup tok =
-  if Token.keyword_with (not o Symbol.is_ascii_identifier) tok
-  then (Markup.operator, "")
-  else
-    let
-      val kind = Token.kind_of tok;
-      val props =
-        if kind = Token.Command
-        then Markup.properties [(Markup.nameN, Token.content_of tok)]
-        else I;
-      val (markup, txt) = token_kind_markup kind;
-    in (props markup, txt) end;
-
 fun reports_of_token tok =
   let
     val malformed_symbols =
@@ -85,7 +50,7 @@
           if Symbol.is_malformed sym
           then SOME ((pos, Markup.bad), "Malformed symbolic character") else NONE);
     val is_malformed = Token.is_error tok orelse not (null malformed_symbols);
-    val (markup, txt) = token_markup tok;
+    val (markup, txt) = Token.markup tok;
     val reports = ((Token.pos_of tok, markup), txt) :: malformed_symbols;
   in (is_malformed, reports) end;
 
@@ -96,7 +61,7 @@
   in (exists fst results, maps snd results) end;
 
 fun present_token tok =
-  Markup.enclose (fst (token_markup tok)) (Output.output (Token.unparse tok));
+  Markup.enclose (fst (Token.markup tok)) (Output.output (Token.unparse tok));
 
 end;