more direct HTML presentation, without print mode;
authorwenzelm
Fri Oct 09 21:16:00 2015 +0200 (2015-10-09 ago)
changeset 61379c57820ceead3
parent 61378 3e04c9ca001a
child 61380 3907f20bef8c
more direct HTML presentation, without print mode;
src/Pure/PIDE/command.ML
src/Pure/PIDE/resources.ML
src/Pure/Thy/html.ML
src/Pure/Thy/thy_syntax.ML
     1.1 --- a/src/Pure/PIDE/command.ML	Fri Oct 09 20:26:03 2015 +0200
     1.2 +++ b/src/Pure/PIDE/command.ML	Fri Oct 09 21:16:00 2015 +0200
     1.3 @@ -109,6 +109,17 @@
     1.4        | NONE => toks)
     1.5    | _ => toks);
     1.6  
     1.7 +fun reports_of_token keywords tok =
     1.8 +  let
     1.9 +    val malformed_symbols =
    1.10 +      Input.source_explode (Token.input_of tok)
    1.11 +      |> map_filter (fn (sym, pos) =>
    1.12 +          if Symbol.is_malformed sym
    1.13 +          then SOME ((pos, Markup.bad), "Malformed symbolic character") else NONE);
    1.14 +    val is_malformed = Token.is_error tok orelse not (null malformed_symbols);
    1.15 +    val reports = Token.reports keywords tok @ Token.completion_report tok @ malformed_symbols;
    1.16 +  in (is_malformed, reports) end;
    1.17 +
    1.18  in
    1.19  
    1.20  fun read_thy st = Toplevel.theory_of st
    1.21 @@ -124,10 +135,10 @@
    1.22          SOME tok => Token.pos_of tok
    1.23        | NONE => #1 proper_range);
    1.24  
    1.25 -    val (is_malformed, token_reports) = Thy_Syntax.reports_of_tokens keywords span;
    1.26 -    val _ = Position.reports_text (token_reports @ maps command_reports span);
    1.27 +    val token_reports = map (reports_of_token keywords) span;
    1.28 +    val _ = Position.reports_text (maps #2 token_reports @ maps command_reports span);
    1.29    in
    1.30 -    if is_malformed then Toplevel.malformed pos "Malformed command syntax"
    1.31 +    if exists #1 token_reports then Toplevel.malformed pos "Malformed command syntax"
    1.32      else
    1.33        (case Outer_Syntax.parse_tokens thy (resolve_files keywords master_dir blobs_info span) of
    1.34          [tr] => Toplevel.modify_init init tr
     2.1 --- a/src/Pure/PIDE/resources.ML	Fri Oct 09 20:26:03 2015 +0200
     2.2 +++ b/src/Pure/PIDE/resources.ML	Fri Oct 09 21:16:00 2015 +0200
     2.3 @@ -159,7 +159,7 @@
     2.4      fun init () =
     2.5        begin_theory master_dir header parents
     2.6        |> Present.begin_theory update_time
     2.7 -          (fn () => HTML.html_mode (implode o map (Thy_Syntax.present_span keywords)) spans);
     2.8 +        (fn () => implode (map (HTML.present_span keywords) spans));
     2.9  
    2.10      val (results, thy) =
    2.11        cond_timeit true ("theory " ^ quote name)
     3.1 --- a/src/Pure/Thy/html.ML	Fri Oct 09 20:26:03 2015 +0200
     3.2 +++ b/src/Pure/Thy/html.ML	Fri Oct 09 21:16:00 2015 +0200
     3.3 @@ -6,9 +6,9 @@
     3.4  
     3.5  signature HTML =
     3.6  sig
     3.7 -  val html_mode: ('a -> 'b) -> 'a -> 'b
     3.8    val reset_symbols: unit -> unit
     3.9    val init_symbols: (string * int) list -> unit
    3.10 +  val present_span: Keyword.keywords -> Command_Span.span -> Output.output
    3.11    type text = string
    3.12    val plain: string -> text
    3.13    val name: string -> text
    3.14 @@ -29,27 +29,17 @@
    3.15  struct
    3.16  
    3.17  
    3.18 -(** HTML print modes **)
    3.19 -
    3.20 -(* mode *)
    3.21 -
    3.22 -val htmlN = "HTML";
    3.23 -fun html_mode f x = Print_Mode.with_modes [htmlN] f x;
    3.24 -
    3.25 -
    3.26  (* common markup *)
    3.27  
    3.28  fun span class = ("<span class=" ^ quote (XML.text class) ^ ">", "</span>");
    3.29  
    3.30 -val _ = Markup.add_mode htmlN (span o fst);
    3.31 +val hidden = span Markup.hiddenN |-> enclose;
    3.32  
    3.33  
    3.34  (* symbol output *)
    3.35  
    3.36  local
    3.37  
    3.38 -val hidden = span Markup.hiddenN |-> enclose;
    3.39 -
    3.40  val symbols =
    3.41    Synchronized.var "HTML.symbols" (NONE: (int * string) Symtab.table option);
    3.42  
    3.43 @@ -87,9 +77,6 @@
    3.44  fun output_width str = output_syms (Symbol.explode str) ([], 0);
    3.45  val output = #1 o output_width;
    3.46  
    3.47 -val _ = Output.add_mode htmlN output_width Symbol.encode_raw;
    3.48 -
    3.49 -
    3.50  fun reset_symbols () = Synchronized.change symbols (K NONE);
    3.51  
    3.52  fun init_symbols codes =
    3.53 @@ -107,6 +94,16 @@
    3.54  end;
    3.55  
    3.56  
    3.57 +(* presentation *)
    3.58 +
    3.59 +fun present_token keywords tok =
    3.60 +  fold_rev (uncurry enclose o span o #1)
    3.61 +    (Token.markups keywords tok) (output (Token.unparse tok));
    3.62 +
    3.63 +fun present_span keywords =
    3.64 +  implode o map (present_token keywords) o Command_Span.content;
    3.65 +
    3.66 +
    3.67  
    3.68  (** HTML markup **)
    3.69  
     4.1 --- a/src/Pure/Thy/thy_syntax.ML	Fri Oct 09 20:26:03 2015 +0200
     4.2 +++ b/src/Pure/Thy/thy_syntax.ML	Fri Oct 09 21:16:00 2015 +0200
     4.3 @@ -1,14 +1,11 @@
     4.4  (*  Title:      Pure/Thy/thy_syntax.ML
     4.5      Author:     Makarius
     4.6  
     4.7 -Superficial theory syntax: tokens and spans.
     4.8 +Theory syntax elements.
     4.9  *)
    4.10  
    4.11  signature THY_SYNTAX =
    4.12  sig
    4.13 -  val reports_of_tokens: Keyword.keywords -> Token.T list -> bool * Position.report_text list
    4.14 -  val present_token: Keyword.keywords -> Token.T -> Output.output
    4.15 -  val present_span: Keyword.keywords -> Command_Span.span -> Output.output
    4.16    datatype 'a element = Element of 'a * ('a element list * 'a) option
    4.17    val atom: 'a -> 'a element
    4.18    val map_element: ('a -> 'b) -> 'a element -> 'b element
    4.19 @@ -20,37 +17,7 @@
    4.20  structure Thy_Syntax: THY_SYNTAX =
    4.21  struct
    4.22  
    4.23 -(** presentation **)
    4.24 -
    4.25 -local
    4.26 -
    4.27 -fun reports_of_token keywords tok =
    4.28 -  let
    4.29 -    val malformed_symbols =
    4.30 -      Input.source_explode (Token.input_of tok)
    4.31 -      |> map_filter (fn (sym, pos) =>
    4.32 -          if Symbol.is_malformed sym
    4.33 -          then SOME ((pos, Markup.bad), "Malformed symbolic character") else NONE);
    4.34 -    val is_malformed = Token.is_error tok orelse not (null malformed_symbols);
    4.35 -    val reports = Token.reports keywords tok @ Token.completion_report tok @ malformed_symbols;
    4.36 -  in (is_malformed, reports) end;
    4.37 -
    4.38 -in
    4.39 -
    4.40 -fun reports_of_tokens keywords toks =
    4.41 -  let val results = map (reports_of_token keywords) toks
    4.42 -  in (exists fst results, maps snd results) end;
    4.43 -
    4.44 -end;
    4.45 -
    4.46 -fun present_token keywords tok =
    4.47 -  fold_rev Markup.enclose (Token.markups keywords tok) (Output.output (Token.unparse tok));
    4.48 -
    4.49 -fun present_span keywords = implode o map (present_token keywords) o Command_Span.content;
    4.50 -
    4.51 -
    4.52 -
    4.53 -(** specification elements: commands with optional proof **)
    4.54 +(* datatype element: command with optional proof *)
    4.55  
    4.56  datatype 'a element = Element of 'a * ('a element list * 'a) option;
    4.57