imitate command markup and rendering of Isabelle/jEdit in HTML output;
authorwenzelm
Tue Dec 09 22:13:48 2014 +0100 (2014-12-09)
changeset 59123e68e44836d04
parent 59122 c1dbcde94cd2
child 59124 60c134fdd290
imitate command markup and rendering of Isabelle/jEdit in HTML output;
etc/isabelle.css
src/Pure/Isar/keyword.ML
src/Pure/Isar/token.ML
src/Pure/PIDE/command.ML
src/Pure/PIDE/resources.ML
src/Pure/Thy/latex.ML
src/Pure/Thy/thy_syntax.ML
     1.1 --- a/etc/isabelle.css	Tue Dec 09 21:14:11 2014 +0100
     1.2 +++ b/etc/isabelle.css	Tue Dec 09 22:13:48 2014 +0100
     1.3 @@ -36,9 +36,8 @@
     1.4  .bold           { font-weight: bold; }
     1.5  
     1.6  .keyword1       { color: #006699; font-weight: bold; }
     1.7 -.command        { color: #006699; font-weight: bold; }
     1.8  .keyword2       { color: #009966; font-weight: bold; }
     1.9 -.keyword        { color: #009966; font-weight: bold; }
    1.10 +.keyword3       { color: #0099FF; font-weight: bold; }
    1.11  .operator       { }
    1.12  .string         { color: #FF00CC; }
    1.13  .alt_string     { color: #CC00CC; }
     2.1 --- a/src/Pure/Isar/keyword.ML	Tue Dec 09 21:14:11 2014 +0100
     2.2 +++ b/src/Pure/Isar/keyword.ML	Tue Dec 09 22:13:48 2014 +0100
     2.3 @@ -41,6 +41,7 @@
     2.4    val is_keyword: keywords -> string -> bool
     2.5    val is_command: keywords -> string -> bool
     2.6    val is_literal: keywords -> string -> bool
     2.7 +  val command_kind: keywords -> string -> string option
     2.8    val command_files: keywords -> string -> Path.T -> Path.T list
     2.9    val command_tags: keywords -> string -> string list
    2.10    val is_vacuous: keywords -> string -> bool
    2.11 @@ -177,10 +178,12 @@
    2.12  
    2.13  (* command kind *)
    2.14  
    2.15 -fun command_kind (Keywords {commands, ...}) = Symtab.lookup commands;
    2.16 +fun lookup_command (Keywords {commands, ...}) = Symtab.lookup commands;
    2.17 +
    2.18 +fun command_kind keywords = Option.map #kind o lookup_command keywords;
    2.19  
    2.20  fun command_files keywords name path =
    2.21 -  (case command_kind keywords name of
    2.22 +  (case lookup_command keywords name of
    2.23      NONE => []
    2.24    | SOME {kind, files, ...} =>
    2.25        if kind <> thy_load then []
    2.26 @@ -188,7 +191,7 @@
    2.27        else map (fn ext => Path.ext ext path) files);
    2.28  
    2.29  fun command_tags keywords name =
    2.30 -  (case command_kind keywords name of
    2.31 +  (case lookup_command keywords name of
    2.32      SOME {tags, ...} => tags
    2.33    | NONE => []);
    2.34  
    2.35 @@ -199,7 +202,7 @@
    2.36    let
    2.37      val tab = Symtab.make_set ks;
    2.38      fun pred keywords name =
    2.39 -      (case command_kind keywords name of
    2.40 +      (case lookup_command keywords name of
    2.41          NONE => false
    2.42        | SOME {kind, ...} => Symtab.defined tab kind);
    2.43    in pred end;
     3.1 --- a/src/Pure/Isar/token.ML	Tue Dec 09 21:14:11 2014 +0100
     3.2 +++ b/src/Pure/Isar/token.ML	Tue Dec 09 22:13:48 2014 +0100
     3.3 @@ -60,8 +60,8 @@
     3.4    val content_of: T -> string
     3.5    val keyword_markup: bool * Markup.T -> string -> Markup.T
     3.6    val completion_report: T -> Position.report_text list
     3.7 -  val report: T -> Position.report_text
     3.8 -  val markup: T -> Markup.T
     3.9 +  val report: Keyword.keywords -> T -> Position.report_text
    3.10 +  val markup: Keyword.keywords -> T -> Markup.T
    3.11    val unparse: T -> string
    3.12    val unparse_src: src -> string list
    3.13    val print: T -> string
    3.14 @@ -233,6 +233,7 @@
    3.15  fun is_kind k (Token (_, (k', _), _)) = k = k';
    3.16  
    3.17  val is_command = is_kind Command;
    3.18 +
    3.19  val is_name = is_kind Ident orf is_kind Sym_Ident orf is_kind String orf is_kind Nat;
    3.20  
    3.21  fun keyword_with pred (Token (_, (Keyword, x), _)) = pred x
    3.22 @@ -293,7 +294,7 @@
    3.23  local
    3.24  
    3.25  val token_kind_markup =
    3.26 - fn Command => (Markup.command, "")
    3.27 + fn Command => (Markup.keyword1, "")
    3.28    | Keyword => (Markup.keyword2, "")
    3.29    | Ident => (Markup.empty, "")
    3.30    | Long_Ident => (Markup.empty, "")
    3.31 @@ -313,6 +314,16 @@
    3.32    | Internal_Value => (Markup.empty, "")
    3.33    | EOF => (Markup.empty, "");
    3.34  
    3.35 +fun keyword_report tok markup = ((pos_of tok, markup), "");
    3.36 +
    3.37 +fun command_markup keywords x =
    3.38 +  (case Keyword.command_kind keywords x of
    3.39 +    SOME k =>
    3.40 +      if k = Keyword.thy_end then Markup.keyword2
    3.41 +      else if k = Keyword.prf_asm orelse k = Keyword.prf_asm_goal then Markup.keyword3
    3.42 +      else Markup.keyword1
    3.43 +  | NONE => Markup.keyword1);
    3.44 +
    3.45  in
    3.46  
    3.47  fun keyword_markup (important, keyword) x =
    3.48 @@ -323,14 +334,16 @@
    3.49    then map (fn m => ((pos_of tok, m), "")) (Completion.suppress_abbrevs (content_of tok))
    3.50    else [];
    3.51  
    3.52 -fun report tok =
    3.53 -  if is_kind Keyword tok then
    3.54 -    ((pos_of tok, keyword_markup (false, Markup.keyword2) (content_of tok)), "")
    3.55 +fun report keywords tok =
    3.56 +  if is_command tok then
    3.57 +    keyword_report tok (command_markup keywords (content_of tok))
    3.58 +  else if is_kind Keyword tok then
    3.59 +    keyword_report tok (keyword_markup (false, Markup.keyword2) (content_of tok))
    3.60    else
    3.61      let val (m, text) = token_kind_markup (kind_of tok)
    3.62      in ((pos_of tok, m), text) end;
    3.63  
    3.64 -val markup = #2 o #1 o report;
    3.65 +fun markup keywords = #2 o #1 o report keywords;
    3.66  
    3.67  end;
    3.68  
    3.69 @@ -349,12 +362,12 @@
    3.70  
    3.71  fun unparse_src (Src {args, ...}) = map unparse args;
    3.72  
    3.73 -fun print tok = Markup.markup (markup tok) (unparse tok);
    3.74 +fun print tok = Markup.markup (markup Keyword.empty_keywords tok) (unparse tok);
    3.75  
    3.76  fun text_of tok =
    3.77    let
    3.78      val k = str_of_kind (kind_of tok);
    3.79 -    val m = markup tok;
    3.80 +    val m = markup Keyword.empty_keywords tok;
    3.81      val s = unparse tok;
    3.82    in
    3.83      if s = "" then (k, "")
    3.84 @@ -451,7 +464,7 @@
    3.85    | SOME (Term t) => Syntax.pretty_term ctxt t
    3.86    | SOME (Fact (_, ths)) =>
    3.87        Pretty.enclose "(" ")" (Pretty.breaks (map (Pretty.backquote o Display.pretty_thm ctxt) ths))
    3.88 -  | _ => Pretty.mark_str (markup tok, unparse tok));
    3.89 +  | _ => Pretty.mark_str (markup Keyword.empty_keywords tok, unparse tok));
    3.90  
    3.91  fun pretty_src ctxt src =
    3.92    let
     4.1 --- a/src/Pure/PIDE/command.ML	Tue Dec 09 21:14:11 2014 +0100
     4.2 +++ b/src/Pure/PIDE/command.ML	Tue Dec 09 22:13:48 2014 +0100
     4.3 @@ -162,7 +162,7 @@
     4.4          SOME tok => Token.pos_of tok
     4.5        | NONE => #1 proper_range);
     4.6  
     4.7 -    val (is_malformed, token_reports) = Thy_Syntax.reports_of_tokens span;
     4.8 +    val (is_malformed, token_reports) = Thy_Syntax.reports_of_tokens keywords span;
     4.9      val _ = Position.reports_text (token_reports @ maps command_reports span);
    4.10    in
    4.11      if is_malformed then Toplevel.malformed pos "Malformed command syntax"
     5.1 --- a/src/Pure/PIDE/resources.ML	Tue Dec 09 21:14:11 2014 +0100
     5.2 +++ b/src/Pure/PIDE/resources.ML	Tue Dec 09 22:13:48 2014 +0100
     5.3 @@ -158,7 +158,7 @@
     5.4      fun init () =
     5.5        begin_theory master_dir header parents
     5.6        |> Present.begin_theory update_time
     5.7 -          (fn () => HTML.html_mode (implode o map Thy_Syntax.present_span) spans);
     5.8 +          (fn () => HTML.html_mode (implode o map (Thy_Syntax.present_span keywords)) spans);
     5.9  
    5.10      val (results, thy) =
    5.11        cond_timeit true ("theory " ^ quote name)
     6.1 --- a/src/Pure/Thy/latex.ML	Tue Dec 09 21:14:11 2014 +0100
     6.2 +++ b/src/Pure/Thy/latex.ML	Tue Dec 09 22:13:48 2014 +0100
     6.3 @@ -189,8 +189,10 @@
     6.4    in (output_symbols syms, Symbol.length syms) end;
     6.5  
     6.6  fun latex_markup (s, _) =
     6.7 -  if s = Markup.commandN orelse s = Markup.keyword1N then ("\\isacommand{", "}")
     6.8 -  else if s = Markup.keyword2N then ("\\isakeyword{", "}")
     6.9 +  if s = Markup.commandN orelse s = Markup.keyword1N orelse s = Markup.keyword3N
    6.10 +  then ("\\isacommand{", "}")
    6.11 +  else if s = Markup.keyword2N
    6.12 +  then ("\\isakeyword{", "}")
    6.13    else Markup.no_output;
    6.14  
    6.15  fun latex_indent "" _ = ""
     7.1 --- a/src/Pure/Thy/thy_syntax.ML	Tue Dec 09 21:14:11 2014 +0100
     7.2 +++ b/src/Pure/Thy/thy_syntax.ML	Tue Dec 09 22:13:48 2014 +0100
     7.3 @@ -6,9 +6,9 @@
     7.4  
     7.5  signature THY_SYNTAX =
     7.6  sig
     7.7 -  val reports_of_tokens: Token.T list -> bool * Position.report_text list
     7.8 -  val present_token: Token.T -> Output.output
     7.9 -  val present_span: Command_Span.span -> Output.output
    7.10 +  val reports_of_tokens: Keyword.keywords -> Token.T list -> bool * Position.report_text list
    7.11 +  val present_token: Keyword.keywords -> Token.T -> Output.output
    7.12 +  val present_span: Keyword.keywords -> Command_Span.span -> Output.output
    7.13    datatype 'a element = Element of 'a * ('a element list * 'a) option
    7.14    val atom: 'a -> 'a element
    7.15    val map_element: ('a -> 'b) -> 'a element -> 'b element
    7.16 @@ -24,7 +24,7 @@
    7.17  
    7.18  local
    7.19  
    7.20 -fun reports_of_token tok =
    7.21 +fun reports_of_token keywords tok =
    7.22    let
    7.23      val malformed_symbols =
    7.24        Input.source_explode (Token.source_position_of tok)
    7.25 @@ -32,21 +32,21 @@
    7.26            if Symbol.is_malformed sym
    7.27            then SOME ((pos, Markup.bad), "Malformed symbolic character") else NONE);
    7.28      val is_malformed = Token.is_error tok orelse not (null malformed_symbols);
    7.29 -    val reports = Token.report tok :: Token.completion_report tok @ malformed_symbols;
    7.30 +    val reports = Token.report keywords tok :: Token.completion_report tok @ malformed_symbols;
    7.31    in (is_malformed, reports) end;
    7.32  
    7.33  in
    7.34  
    7.35 -fun reports_of_tokens toks =
    7.36 -  let val results = map reports_of_token toks
    7.37 +fun reports_of_tokens keywords toks =
    7.38 +  let val results = map (reports_of_token keywords) toks
    7.39    in (exists fst results, maps snd results) end;
    7.40  
    7.41  end;
    7.42  
    7.43 -fun present_token tok =
    7.44 -  Markup.enclose (Token.markup tok) (Output.output (Token.unparse tok));
    7.45 +fun present_token keywords tok =
    7.46 +  Markup.enclose (Token.markup keywords tok) (Output.output (Token.unparse tok));
    7.47  
    7.48 -val present_span = implode o map present_token o Command_Span.content;
    7.49 +fun present_span keywords = implode o map (present_token keywords) o Command_Span.content;
    7.50  
    7.51  
    7.52