--- 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; }
--- 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;
--- 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
--- 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"
--- 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)
--- 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 "" _ = ""
--- 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;