# HG changeset patch
# User wenzelm
# Date 1275221670 -7200
# Node ID 8cdddd689ea98de1989786737764abab2b296290
# Parent  beb9a869526370b402089c88c9c0ab98f97f114b
markup non-identifier keyword as operator;

diff -r beb9a8695263 -r 8cdddd689ea9 lib/html/isabelle.css
--- a/lib/html/isabelle.css	Sun May 30 13:47:12 2010 +0200
+++ b/lib/html/isabelle.css	Sun May 30 14:14:30 2010 +0200
@@ -38,6 +38,7 @@
 .loc, loc  { color: #D2691E; }
 
 .keyword, keyword      { font-weight: bold; }
+.operator, operator    { }
 .command, command      { font-weight: bold; }
 .ident, ident          { }
 .string, string        { color: #008B00; }
diff -r beb9a8695263 -r 8cdddd689ea9 src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Sun May 30 13:47:12 2010 +0200
+++ b/src/Pure/General/markup.ML	Sun May 30 14:14:30 2010 +0200
@@ -83,6 +83,7 @@
   val keyword_declN: string val keyword_decl: string -> T
   val command_declN: string val command_decl: string -> string -> T
   val keywordN: string val keyword: string -> T
+  val operatorN: string val operator: T
   val commandN: string val command: string -> T
   val identN: string val ident: T
   val stringN: string val string: T
@@ -271,6 +272,7 @@
 fun command_decl name kind : T = (command_declN, [(nameN, name), (kindN, kind)]);
 
 val (keywordN, keyword) = markup_string "keyword" nameN;
+val (operatorN, operator) = markup_elem "operator";
 val (commandN, command) = markup_string "command" nameN;
 val (identN, ident) = markup_elem "ident";
 val (stringN, string) = markup_elem "string";
diff -r beb9a8695263 -r 8cdddd689ea9 src/Pure/Thy/thy_syntax.ML
--- a/src/Pure/Thy/thy_syntax.ML	Sun May 30 13:47:12 2010 +0200
+++ b/src/Pure/Thy/thy_syntax.ML	Sun May 30 14:14:30 2010 +0200
@@ -67,13 +67,17 @@
   | Token.Sync          => Markup.control
   | Token.EOF           => Markup.control;
 
+fun token_markup tok =
+  if Token.keyword_with (not o Syntax.is_identifier) tok then Markup.operator
+  else token_kind_markup (Token.kind_of tok);
+
 in
 
 fun present_token tok =
-  Markup.enclose (token_kind_markup (Token.kind_of tok)) (Output.output (Token.unparse tok));
+  Markup.enclose (token_markup tok) (Output.output (Token.unparse tok));
 
 fun report_token tok =
-  Position.report (token_kind_markup (Token.kind_of tok)) (Token.position_of tok);
+  Position.report (token_markup tok) (Token.position_of tok);
 
 end;