more direct HTML presentation, without print mode;

--- a/src/Pure/PIDE/command.ML	Fri Oct 09 20:26:03 2015 +0200
+++ b/src/Pure/PIDE/command.ML	Fri Oct 09 21:16:00 2015 +0200
@@ -109,6 +109,17 @@
       | NONE => toks)
   | _ => toks);
 
+fun reports_of_token keywords tok =
+  let
+    val malformed_symbols =
+      Input.source_explode (Token.input_of tok)
+      |> map_filter (fn (sym, pos) =>
+          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.reports keywords tok @ Token.completion_report tok @ malformed_symbols;
+  in (is_malformed, reports) end;
+
 in
 
 fun read_thy st = Toplevel.theory_of st
@@ -124,10 +135,10 @@
         SOME tok => Token.pos_of tok
       | NONE => #1 proper_range);
 
-    val (is_malformed, token_reports) = Thy_Syntax.reports_of_tokens keywords span;
-    val _ = Position.reports_text (token_reports @ maps command_reports span);
+    val token_reports = map (reports_of_token keywords) span;
+    val _ = Position.reports_text (maps #2 token_reports @ maps command_reports span);
   in
-    if is_malformed then Toplevel.malformed pos "Malformed command syntax"
+    if exists #1 token_reports then Toplevel.malformed pos "Malformed command syntax"
     else
       (case Outer_Syntax.parse_tokens thy (resolve_files keywords master_dir blobs_info span) of
         [tr] => Toplevel.modify_init init tr

--- a/src/Pure/PIDE/resources.ML	Fri Oct 09 20:26:03 2015 +0200
+++ b/src/Pure/PIDE/resources.ML	Fri Oct 09 21:16:00 2015 +0200
@@ -159,7 +159,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 keywords)) spans);
+        (fn () => implode (map (HTML.present_span keywords) spans));
 
     val (results, thy) =
       cond_timeit true ("theory " ^ quote name)

--- a/src/Pure/Thy/html.ML	Fri Oct 09 20:26:03 2015 +0200
+++ b/src/Pure/Thy/html.ML	Fri Oct 09 21:16:00 2015 +0200
@@ -6,9 +6,9 @@
 
 signature HTML =
 sig
-  val html_mode: ('a -> 'b) -> 'a -> 'b
   val reset_symbols: unit -> unit
   val init_symbols: (string * int) list -> unit
+  val present_span: Keyword.keywords -> Command_Span.span -> Output.output
   type text = string
   val plain: string -> text
   val name: string -> text
@@ -29,27 +29,17 @@
 struct
 
 
-(** HTML print modes **)
-
-(* mode *)
-
-val htmlN = "HTML";
-fun html_mode f x = Print_Mode.with_modes [htmlN] f x;
-
-
 (* common markup *)
 
 fun span class = ("<span class=" ^ quote (XML.text class) ^ ">", "</span>");
 
-val _ = Markup.add_mode htmlN (span o fst);
+val hidden = span Markup.hiddenN |-> enclose;
 
 
 (* symbol output *)
 
 local
 
-val hidden = span Markup.hiddenN |-> enclose;
-
 val symbols =
   Synchronized.var "HTML.symbols" (NONE: (int * string) Symtab.table option);
 
@@ -87,9 +77,6 @@
 fun output_width str = output_syms (Symbol.explode str) ([], 0);
 val output = #1 o output_width;
 
-val _ = Output.add_mode htmlN output_width Symbol.encode_raw;
-
-
 fun reset_symbols () = Synchronized.change symbols (K NONE);
 
 fun init_symbols codes =
@@ -107,6 +94,16 @@
 end;
 
 
+(* presentation *)
+
+fun present_token keywords tok =
+  fold_rev (uncurry enclose o span o #1)
+    (Token.markups keywords tok) (output (Token.unparse tok));
+
+fun present_span keywords =
+  implode o map (present_token keywords) o Command_Span.content;
+
+
 
 (** HTML markup **)
 

--- a/src/Pure/Thy/thy_syntax.ML	Fri Oct 09 20:26:03 2015 +0200
+++ b/src/Pure/Thy/thy_syntax.ML	Fri Oct 09 21:16:00 2015 +0200
@@ -1,14 +1,11 @@
 (*  Title:      Pure/Thy/thy_syntax.ML
     Author:     Makarius
 
-Superficial theory syntax: tokens and spans.
+Theory syntax elements.
 *)
 
 signature THY_SYNTAX =
 sig
-  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
@@ -20,37 +17,7 @@
 structure Thy_Syntax: THY_SYNTAX =
 struct
 
-(** presentation **)
-
-local
-
-fun reports_of_token keywords tok =
-  let
-    val malformed_symbols =
-      Input.source_explode (Token.input_of tok)
-      |> map_filter (fn (sym, pos) =>
-          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.reports keywords tok @ Token.completion_report tok @ malformed_symbols;
-  in (is_malformed, reports) end;
-
-in
-
-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 keywords tok =
-  fold_rev Markup.enclose (Token.markups keywords tok) (Output.output (Token.unparse tok));
-
-fun present_span keywords = implode o map (present_token keywords) o Command_Span.content;
-
-
-
-(** specification elements: commands with optional proof **)
+(* datatype element: command with optional proof *)
 
 datatype 'a element = Element of 'a * ('a element list * 'a) option;