# HG changeset patch
# User wenzelm
# Date 1497259943 -7200
# Node ID cdbcb417db67051d0d3860f0588304156727b69c
# Parent  7ac97dea27d2f7a9b8766e8f8e514b00ae6283ba
more markup for HTML rendering;

diff -r 7ac97dea27d2 -r cdbcb417db67 src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Mon Jun 12 10:58:10 2017 +0200
+++ b/src/Pure/Isar/token.ML	Mon Jun 12 11:32:23 2017 +0200
@@ -281,7 +281,7 @@
 fun keyword_reports tok = map (fn markup => ((pos_of tok, markup), ""));
 
 fun command_markups keywords x =
-  if Keyword.is_theory_end keywords x then [Markup.keyword2]
+  if Keyword.is_theory_end keywords x then [Markup.keyword2 |> Markup.keyword_properties]
   else
     (if Keyword.is_proof_asm keywords x then [Markup.keyword3]
      else if Keyword.is_improper keywords x then [Markup.keyword1, Markup.improper]
@@ -303,7 +303,7 @@
     keyword_reports tok (command_markups keywords (content_of tok))
   else if is_kind Keyword tok then
     keyword_reports tok
-      [keyword_markup (false, Markup.keyword_properties Markup.keyword2) (content_of tok)]
+      [keyword_markup (false, Markup.keyword2 |> Markup.keyword_properties) (content_of tok)]
   else
     let val (m, text) = token_kind_markup (kind_of tok)
     in [((pos_of tok, m), text)] end;
diff -r 7ac97dea27d2 -r cdbcb417db67 src/Pure/ML/ml_lex.ML
--- a/src/Pure/ML/ml_lex.ML	Mon Jun 12 10:58:10 2017 +0200
+++ b/src/Pure/ML/ml_lex.ML	Mon Jun 12 11:32:23 2017 +0200
@@ -157,9 +157,9 @@
     val (markup, txt) =
       if not (is_keyword tok) then token_kind_markup SML kind
       else if is_delimiter tok then (Markup.ML_delimiter, "")
-      else if member (op =) keywords2 x then (Markup.ML_keyword2, "")
-      else if member (op =) keywords3 x then (Markup.ML_keyword3, "")
-      else (Markup.ML_keyword1, "");
+      else if member (op =) keywords2 x then (Markup.ML_keyword2 |> Markup.keyword_properties, "")
+      else if member (op =) keywords3 x then (Markup.ML_keyword3 |> Markup.keyword_properties, "")
+      else (Markup.ML_keyword1 |> Markup.keyword_properties, "");
   in ((pos, markup), txt) end;
 
 end;
diff -r 7ac97dea27d2 -r cdbcb417db67 src/Pure/ML/ml_thms.ML
--- a/src/Pure/ML/ml_thms.ML	Mon Jun 12 10:58:10 2017 +0200
+++ b/src/Pure/ML/ml_thms.ML	Mon Jun 12 11:32:23 2017 +0200
@@ -85,7 +85,9 @@
       (Parse.position by -- Method.parse -- Scan.option Method.parse)))
     (fn _ => fn ((is_open, raw_propss), (((_, by_pos), m1), m2)) => fn ctxt =>
       let
-        val reports = (by_pos, Markup.keyword1) :: maps Method.reports_of (m1 :: the_list m2);
+        val reports =
+          (by_pos, Markup.keyword1 |> Markup.keyword_properties) ::
+            maps Method.reports_of (m1 :: the_list m2);
         val _ = Context_Position.reports ctxt reports;
 
         val propss = burrow (map (rpair []) o Syntax.read_props ctxt) raw_propss;
diff -r 7ac97dea27d2 -r cdbcb417db67 src/Pure/Thy/document_antiquotations.ML
--- a/src/Pure/Thy/document_antiquotations.ML	Mon Jun 12 10:58:10 2017 +0200
+++ b/src/Pure/Thy/document_antiquotations.ML	Mon Jun 12 11:32:23 2017 +0200
@@ -136,7 +136,9 @@
       Scan.lift (Parse.position (Parse.reserved "by") -- Method.parse -- Scan.option Method.parse))
     (fn {source, context = ctxt, ...} => fn ((prop_token, prop), (((_, by_pos), m1), m2)) =>
       let
-        val reports = (by_pos, Markup.keyword1) :: maps Method.reports_of (m1 :: the_list m2);
+        val reports =
+          (by_pos, Markup.keyword1 |> Markup.keyword_properties) ::
+            maps Method.reports_of (m1 :: the_list m2);
         val _ = Context_Position.reports ctxt reports;
 
         (* FIXME check proof!? *)