# HG changeset patch # User wenzelm # Date 1418215544 -3600 # Node ID ee19c92ae8b4d5931415d945450d0969be2d34c0 # Parent 60c134fdd29033ea979636323cdb0371835898d9 more explicit markup for improper commands; clarified CSS rendering; diff -r 60c134fdd290 -r ee19c92ae8b4 etc/isabelle.css --- a/etc/isabelle.css Wed Dec 10 10:44:56 2014 +0100 +++ b/etc/isabelle.css Wed Dec 10 13:45:44 2014 +0100 @@ -44,9 +44,6 @@ .verbatim { color: #6600CC; } .cartouche { color: #CC6600; } .comment { color: #CC0000; } -.control { background-color: #FF6A6A; } +.improper { color: #FF5050; } .bad { background-color: #FF6A6A; } -.keyword1 { font-weight: bold; } -.keyword2 { font-weight: bold; } - diff -r 60c134fdd290 -r ee19c92ae8b4 src/Pure/Isar/keyword.ML --- a/src/Pure/Isar/keyword.ML Wed Dec 10 10:44:56 2014 +0100 +++ b/src/Pure/Isar/keyword.ML Wed Dec 10 13:45:44 2014 +0100 @@ -51,6 +51,7 @@ val is_document_raw: keywords -> string -> bool val is_document: keywords -> string -> bool val is_theory_begin: keywords -> string -> bool + val is_theory_end: keywords -> string -> bool val is_theory_load: keywords -> string -> bool val is_theory: keywords -> string -> bool val is_theory_body: keywords -> string -> bool @@ -60,6 +61,8 @@ val is_proof_goal: keywords -> string -> bool val is_qed: keywords -> string -> bool val is_qed_global: keywords -> string -> bool + val is_proof_asm: keywords -> string -> bool + val is_improper: keywords -> string -> bool val is_printed: keywords -> string -> bool end; @@ -217,6 +220,7 @@ val is_document = command_category [document_heading, document_body, document_raw]; val is_theory_begin = command_category [thy_begin]; +val is_theory_end = command_category [thy_end]; val is_theory_load = command_category [thy_load]; @@ -239,6 +243,9 @@ val is_qed = command_category [qed, qed_script, qed_block]; val is_qed_global = command_category [qed_global]; +val is_proof_asm = command_category [prf_asm, prf_asm_goal]; +val is_improper = command_category [qed_script, prf_script, prf_asm_goal_script]; + fun is_printed keywords = is_theory_goal keywords orf is_proof keywords; end; diff -r 60c134fdd290 -r ee19c92ae8b4 src/Pure/Isar/token.ML --- a/src/Pure/Isar/token.ML Wed Dec 10 10:44:56 2014 +0100 +++ b/src/Pure/Isar/token.ML Wed Dec 10 13:45:44 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: Keyword.keywords -> T -> Position.report_text - val markup: Keyword.keywords -> T -> Markup.T + val reports: Keyword.keywords -> T -> Position.report_text list + val markups: Keyword.keywords -> T -> Markup.T list val unparse: T -> string val unparse_src: src -> string list val print: T -> string @@ -305,15 +305,13 @@ | Error msg => (Markup.bad, msg) | _ => (Markup.empty, ""); -fun keyword_report tok markup = ((pos_of tok, markup), ""); +fun keyword_reports tok = map (fn 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); +fun command_markups keywords x = + if Keyword.is_theory_end keywords x then [Markup.keyword2] + else if Keyword.is_proof_asm keywords x then [Markup.keyword3] + else if Keyword.is_improper keywords x then [Markup.keyword1, Markup.improper] + else [Markup.keyword1]; in @@ -325,16 +323,16 @@ then map (fn m => ((pos_of tok, m), "")) (Completion.suppress_abbrevs (content_of tok)) else []; -fun report keywords tok = +fun reports keywords tok = if is_command tok then - keyword_report tok (command_markup keywords (content_of tok)) + keyword_reports tok (command_markups keywords (content_of tok)) else if is_kind Keyword tok then - keyword_report tok (keyword_markup (false, Markup.keyword2) (content_of tok)) + keyword_reports 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; + in [((pos_of tok, m), text)] end; -fun markup keywords = #2 o #1 o report keywords; +fun markups keywords = map (#2 o #1) o reports keywords; end; @@ -353,18 +351,18 @@ fun unparse_src (Src {args, ...}) = map unparse args; -fun print tok = Markup.markup (markup Keyword.empty_keywords tok) (unparse tok); +fun print tok = Markup.markups (markups Keyword.empty_keywords tok) (unparse tok); fun text_of tok = let val k = str_of_kind (kind_of tok); - val m = markup Keyword.empty_keywords tok; + val ms = markups Keyword.empty_keywords tok; val s = unparse tok; in if s = "" then (k, "") else if size s < 40 andalso not (exists_string (fn c => c = "\n") s) - then (k ^ " " ^ Markup.markup m s, "") - else (k, Markup.markup m s) + then (k ^ " " ^ Markup.markups ms s, "") + else (k, Markup.markups ms s) end; @@ -455,7 +453,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 Keyword.empty_keywords tok, unparse tok)); + | _ => Pretty.marks_str (markups Keyword.empty_keywords tok, unparse tok)); fun pretty_src ctxt src = let @@ -468,6 +466,7 @@ in Pretty.block (Pretty.breaks (prt_name :: map prt_arg args)) end; + (** scanners **) open Basic_Symbol_Pos; diff -r 60c134fdd290 -r ee19c92ae8b4 src/Pure/PIDE/markup.ML --- a/src/Pure/PIDE/markup.ML Wed Dec 10 10:44:56 2014 +0100 +++ b/src/Pure/PIDE/markup.ML Wed Dec 10 13:45:44 2014 +0100 @@ -202,6 +202,7 @@ val output: T -> Output.output * Output.output val enclose: T -> Output.output -> Output.output val markup: T -> string -> string + val markups: T list -> string -> string val markup_only: T -> string val markup_report: string -> string end; @@ -645,6 +646,8 @@ let val (bg, en) = output m in Library.enclose (Output.escape bg) (Output.escape en) end; +val markups = fold_rev markup; + fun markup_only m = markup m ""; fun markup_report "" = "" diff -r 60c134fdd290 -r ee19c92ae8b4 src/Pure/Thy/thy_syntax.ML --- a/src/Pure/Thy/thy_syntax.ML Wed Dec 10 10:44:56 2014 +0100 +++ b/src/Pure/Thy/thy_syntax.ML Wed Dec 10 13:45:44 2014 +0100 @@ -32,7 +32,7 @@ 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 keywords tok :: Token.completion_report tok @ malformed_symbols; + val reports = Token.reports keywords tok @ Token.completion_report tok @ malformed_symbols; in (is_malformed, reports) end; in @@ -44,7 +44,7 @@ end; fun present_token keywords tok = - Markup.enclose (Token.markup keywords tok) (Output.output (Token.unparse 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; diff -r 60c134fdd290 -r ee19c92ae8b4 src/Tools/jEdit/src/rendering.scala --- a/src/Tools/jEdit/src/rendering.scala Wed Dec 10 10:44:56 2014 +0100 +++ b/src/Tools/jEdit/src/rendering.scala Wed Dec 10 13:45:44 2014 +0100 @@ -53,11 +53,8 @@ import JEditToken._ Map[String, Byte]( Keyword.THY_END -> KEYWORD2, - Keyword.QED_SCRIPT -> DIGIT, - Keyword.PRF_SCRIPT -> DIGIT, Keyword.PRF_ASM -> KEYWORD3, - Keyword.PRF_ASM_GOAL -> KEYWORD3, - Keyword.PRF_ASM_GOAL_SCRIPT -> DIGIT + Keyword.PRF_ASM_GOAL -> KEYWORD3 ).withDefaultValue(KEYWORD1) }