# HG changeset patch
# User wenzelm
# Date 1418159628 -3600
# Node ID e68e44836d0440cae4615018b74e9cb22bc60cb4
# Parent  c1dbcde94cd27a735efab81fed1f74d6fb709acf
imitate command markup and rendering of Isabelle/jEdit in HTML output;

diff -r c1dbcde94cd2 -r e68e44836d04 etc/isabelle.css
--- a/etc/isabelle.css	Tue Dec 09 21:14:11 2014 +0100
+++ b/etc/isabelle.css	Tue Dec 09 22:13:48 2014 +0100
@@ -36,9 +36,8 @@
 .bold           { font-weight: bold; }
 
 .keyword1       { color: #006699; font-weight: bold; }
-.command        { color: #006699; font-weight: bold; }
 .keyword2       { color: #009966; font-weight: bold; }
-.keyword        { color: #009966; font-weight: bold; }
+.keyword3       { color: #0099FF; font-weight: bold; }
 .operator       { }
 .string         { color: #FF00CC; }
 .alt_string     { color: #CC00CC; }
diff -r c1dbcde94cd2 -r e68e44836d04 src/Pure/Isar/keyword.ML
--- a/src/Pure/Isar/keyword.ML	Tue Dec 09 21:14:11 2014 +0100
+++ b/src/Pure/Isar/keyword.ML	Tue Dec 09 22:13:48 2014 +0100
@@ -41,6 +41,7 @@
   val is_keyword: keywords -> string -> bool
   val is_command: keywords -> string -> bool
   val is_literal: keywords -> string -> bool
+  val command_kind: keywords -> string -> string option
   val command_files: keywords -> string -> Path.T -> Path.T list
   val command_tags: keywords -> string -> string list
   val is_vacuous: keywords -> string -> bool
@@ -177,10 +178,12 @@
 
 (* command kind *)
 
-fun command_kind (Keywords {commands, ...}) = Symtab.lookup commands;
+fun lookup_command (Keywords {commands, ...}) = Symtab.lookup commands;
+
+fun command_kind keywords = Option.map #kind o lookup_command keywords;
 
 fun command_files keywords name path =
-  (case command_kind keywords name of
+  (case lookup_command keywords name of
     NONE => []
   | SOME {kind, files, ...} =>
       if kind <> thy_load then []
@@ -188,7 +191,7 @@
       else map (fn ext => Path.ext ext path) files);
 
 fun command_tags keywords name =
-  (case command_kind keywords name of
+  (case lookup_command keywords name of
     SOME {tags, ...} => tags
   | NONE => []);
 
@@ -199,7 +202,7 @@
   let
     val tab = Symtab.make_set ks;
     fun pred keywords name =
-      (case command_kind keywords name of
+      (case lookup_command keywords name of
         NONE => false
       | SOME {kind, ...} => Symtab.defined tab kind);
   in pred end;
diff -r c1dbcde94cd2 -r e68e44836d04 src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Tue Dec 09 21:14:11 2014 +0100
+++ b/src/Pure/Isar/token.ML	Tue Dec 09 22:13:48 2014 +0100
@@ -60,8 +60,8 @@
   val content_of: T -> string
   val keyword_markup: bool * Markup.T -> string -> Markup.T
   val completion_report: T -> Position.report_text list
-  val report: T -> Position.report_text
-  val markup: T -> Markup.T
+  val report: Keyword.keywords -> T -> Position.report_text
+  val markup: Keyword.keywords -> T -> Markup.T
   val unparse: T -> string
   val unparse_src: src -> string list
   val print: T -> string
@@ -233,6 +233,7 @@
 fun is_kind k (Token (_, (k', _), _)) = k = k';
 
 val is_command = is_kind Command;
+
 val is_name = is_kind Ident orf is_kind Sym_Ident orf is_kind String orf is_kind Nat;
 
 fun keyword_with pred (Token (_, (Keyword, x), _)) = pred x
@@ -293,7 +294,7 @@
 local
 
 val token_kind_markup =
- fn Command => (Markup.command, "")
+ fn Command => (Markup.keyword1, "")
   | Keyword => (Markup.keyword2, "")
   | Ident => (Markup.empty, "")
   | Long_Ident => (Markup.empty, "")
@@ -313,6 +314,16 @@
   | Internal_Value => (Markup.empty, "")
   | EOF => (Markup.empty, "");
 
+fun keyword_report tok markup = ((pos_of tok, markup), "");
+
+fun command_markup keywords x =
+  (case Keyword.command_kind keywords x of
+    SOME k =>
+      if k = Keyword.thy_end then Markup.keyword2
+      else if k = Keyword.prf_asm orelse k = Keyword.prf_asm_goal then Markup.keyword3
+      else Markup.keyword1
+  | NONE => Markup.keyword1);
+
 in
 
 fun keyword_markup (important, keyword) x =
@@ -323,14 +334,16 @@
   then map (fn m => ((pos_of tok, m), "")) (Completion.suppress_abbrevs (content_of tok))
   else [];
 
-fun report tok =
-  if is_kind Keyword tok then
-    ((pos_of tok, keyword_markup (false, Markup.keyword2) (content_of tok)), "")
+fun report keywords tok =
+  if is_command tok then
+    keyword_report tok (command_markup keywords (content_of tok))
+  else if is_kind Keyword tok then
+    keyword_report tok (keyword_markup (false, Markup.keyword2) (content_of tok))
   else
     let val (m, text) = token_kind_markup (kind_of tok)
     in ((pos_of tok, m), text) end;
 
-val markup = #2 o #1 o report;
+fun markup keywords = #2 o #1 o report keywords;
 
 end;
 
@@ -349,12 +362,12 @@
 
 fun unparse_src (Src {args, ...}) = map unparse args;
 
-fun print tok = Markup.markup (markup tok) (unparse tok);
+fun print tok = Markup.markup (markup Keyword.empty_keywords tok) (unparse tok);
 
 fun text_of tok =
   let
     val k = str_of_kind (kind_of tok);
-    val m = markup tok;
+    val m = markup Keyword.empty_keywords tok;
     val s = unparse tok;
   in
     if s = "" then (k, "")
@@ -451,7 +464,7 @@
   | SOME (Term t) => Syntax.pretty_term ctxt t
   | SOME (Fact (_, ths)) =>
       Pretty.enclose "(" ")" (Pretty.breaks (map (Pretty.backquote o Display.pretty_thm ctxt) ths))
-  | _ => Pretty.mark_str (markup tok, unparse tok));
+  | _ => Pretty.mark_str (markup Keyword.empty_keywords tok, unparse tok));
 
 fun pretty_src ctxt src =
   let
diff -r c1dbcde94cd2 -r e68e44836d04 src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Tue Dec 09 21:14:11 2014 +0100
+++ b/src/Pure/PIDE/command.ML	Tue Dec 09 22:13:48 2014 +0100
@@ -162,7 +162,7 @@
         SOME tok => Token.pos_of tok
       | NONE => #1 proper_range);
 
-    val (is_malformed, token_reports) = Thy_Syntax.reports_of_tokens span;
+    val (is_malformed, token_reports) = Thy_Syntax.reports_of_tokens keywords span;
     val _ = Position.reports_text (token_reports @ maps command_reports span);
   in
     if is_malformed then Toplevel.malformed pos "Malformed command syntax"
diff -r c1dbcde94cd2 -r e68e44836d04 src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Tue Dec 09 21:14:11 2014 +0100
+++ b/src/Pure/PIDE/resources.ML	Tue Dec 09 22:13:48 2014 +0100
@@ -158,7 +158,7 @@
     fun init () =
       begin_theory master_dir header parents
       |> Present.begin_theory update_time
-          (fn () => HTML.html_mode (implode o map Thy_Syntax.present_span) spans);
+          (fn () => HTML.html_mode (implode o map (Thy_Syntax.present_span keywords)) spans);
 
     val (results, thy) =
       cond_timeit true ("theory " ^ quote name)
diff -r c1dbcde94cd2 -r e68e44836d04 src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Tue Dec 09 21:14:11 2014 +0100
+++ b/src/Pure/Thy/latex.ML	Tue Dec 09 22:13:48 2014 +0100
@@ -189,8 +189,10 @@
   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.keyword2N then ("\\isakeyword{", "}")
+  if s = Markup.commandN orelse s = Markup.keyword1N orelse s = Markup.keyword3N
+  then ("\\isacommand{", "}")
+  else if s = Markup.keyword2N
+  then ("\\isakeyword{", "}")
   else Markup.no_output;
 
 fun latex_indent "" _ = ""
diff -r c1dbcde94cd2 -r e68e44836d04 src/Pure/Thy/thy_syntax.ML
--- a/src/Pure/Thy/thy_syntax.ML	Tue Dec 09 21:14:11 2014 +0100
+++ b/src/Pure/Thy/thy_syntax.ML	Tue Dec 09 22:13:48 2014 +0100
@@ -6,9 +6,9 @@
 
 signature THY_SYNTAX =
 sig
-  val reports_of_tokens: Token.T list -> bool * Position.report_text list
-  val present_token: Token.T -> Output.output
-  val present_span: Command_Span.span -> Output.output
+  val reports_of_tokens: Keyword.keywords -> Token.T list -> bool * Position.report_text list
+  val present_token: Keyword.keywords -> Token.T -> Output.output
+  val present_span: Keyword.keywords -> Command_Span.span -> Output.output
   datatype 'a element = Element of 'a * ('a element list * 'a) option
   val atom: 'a -> 'a element
   val map_element: ('a -> 'b) -> 'a element -> 'b element
@@ -24,7 +24,7 @@
 
 local
 
-fun reports_of_token tok =
+fun reports_of_token keywords tok =
   let
     val malformed_symbols =
       Input.source_explode (Token.source_position_of tok)
@@ -32,21 +32,21 @@
           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 reports = Token.report tok :: Token.completion_report tok @ malformed_symbols;
+    val reports = Token.report keywords tok :: Token.completion_report tok @ malformed_symbols;
   in (is_malformed, reports) end;
 
 in
 
-fun reports_of_tokens toks =
-  let val results = map reports_of_token toks
+fun reports_of_tokens keywords toks =
+  let val results = map (reports_of_token keywords) toks
   in (exists fst results, maps snd results) end;
 
 end;
 
-fun present_token tok =
-  Markup.enclose (Token.markup tok) (Output.output (Token.unparse tok));
+fun present_token keywords tok =
+  Markup.enclose (Token.markup keywords tok) (Output.output (Token.unparse tok));
 
-val present_span = implode o map present_token o Command_Span.content;
+fun present_span keywords = implode o map (present_token keywords) o Command_Span.content;