src/Pure/Isar/token.ML
changeset 55744 4a4e5686e091
parent 55709 4e5a83a46ded
child 55745 b865c3035d5c
     1.1 --- a/src/Pure/Isar/token.ML	Tue Feb 25 14:56:58 2014 +0100
     1.2 +++ b/src/Pure/Isar/token.ML	Tue Feb 25 17:03:55 2014 +0100
     1.3 @@ -42,6 +42,7 @@
     1.4    val inner_syntax_of: T -> string
     1.5    val source_position_of: T -> Symbol_Pos.text * Position.T
     1.6    val content_of: T -> string
     1.7 +  val markup: T -> Markup.T * string
     1.8    val unparse: T -> string
     1.9    val text_of: T -> string * string
    1.10    val get_files: T -> file Exn.result list
    1.11 @@ -213,6 +214,42 @@
    1.12  fun content_of (Token (_, (_, x), _)) = x;
    1.13  
    1.14  
    1.15 +(* markup *)
    1.16 +
    1.17 +local
    1.18 +
    1.19 +val token_kind_markup =
    1.20 + fn Command       => (Markup.keyword1, "")
    1.21 +  | Keyword       => (Markup.keyword2, "")
    1.22 +  | Ident         => (Markup.empty, "")
    1.23 +  | LongIdent     => (Markup.empty, "")
    1.24 +  | SymIdent      => (Markup.empty, "")
    1.25 +  | Var           => (Markup.var, "")
    1.26 +  | TypeIdent     => (Markup.tfree, "")
    1.27 +  | TypeVar       => (Markup.tvar, "")
    1.28 +  | Nat           => (Markup.empty, "")
    1.29 +  | Float         => (Markup.empty, "")
    1.30 +  | String        => (Markup.string, "")
    1.31 +  | AltString     => (Markup.altstring, "")
    1.32 +  | Verbatim      => (Markup.verbatim, "")
    1.33 +  | Cartouche     => (Markup.cartouche, "")
    1.34 +  | Space         => (Markup.empty, "")
    1.35 +  | Comment       => (Markup.comment, "")
    1.36 +  | InternalValue => (Markup.empty, "")
    1.37 +  | Error msg     => (Markup.bad, msg)
    1.38 +  | Sync          => (Markup.control, "")
    1.39 +  | EOF           => (Markup.control, "");
    1.40 +
    1.41 +in
    1.42 +
    1.43 +fun markup tok =
    1.44 +  if keyword_with (not o Symbol.is_ascii_identifier) tok
    1.45 +  then (Markup.operator, "")
    1.46 +  else token_kind_markup (kind_of tok);
    1.47 +
    1.48 +end;
    1.49 +
    1.50 +
    1.51  (* unparse *)
    1.52  
    1.53  fun unparse (Token (_, (kind, x), _)) =
    1.54 @@ -231,11 +268,13 @@
    1.55    else
    1.56      let
    1.57        val k = str_of_kind (kind_of tok);
    1.58 +      val (m, _) = markup tok;
    1.59        val s = unparse tok;
    1.60      in
    1.61        if s = "" then (k, "")
    1.62 -      else if size s < 40 andalso not (exists_string (fn c => c = "\n") s) then (k ^ " " ^ s, "")
    1.63 -      else (k, s)
    1.64 +      else if size s < 40 andalso not (exists_string (fn c => c = "\n") s)
    1.65 +      then (k ^ " " ^ Markup.markup m s, "")
    1.66 +      else (k, Markup.markup m s)
    1.67      end;
    1.68  
    1.69