# HG changeset patch # User wenzelm # Date 1394637107 -3600 # Node ID 38f13d0551078b547f45c31fc334124e17f5dd29 # Parent 8ae2965ddc80f4c334c5b34eeb2425380ed6449a more explicit markup for Token.Literal; Markup.quasi_keyword for Parse.$$$ -- it is used within Args.syntax as well; Markup.operator for name of Args.syntax, to override outer keywords like "where"; tuned signature; diff -r 8ae2965ddc80 -r 38f13d055107 src/Pure/Isar/args.ML --- a/src/Pure/Isar/args.ML Wed Mar 12 14:37:14 2014 +0100 +++ b/src/Pure/Isar/args.ML Wed Mar 12 16:11:47 2014 +0100 @@ -102,7 +102,9 @@ val prt_thm = Pretty.backquote o Display.pretty_thm ctxt; fun prt_arg arg = (case Token.get_value arg of - SOME (v as Token.Literal s) => Pretty.marks_str (Token.value_markup v, s) + SOME (Token.Literal markup) => + let val x = Token.content_of arg + in Pretty.mark_str (Token.keyword_markup markup x, x) end | SOME (Token.Text s) => Pretty.str (quote s) | SOME (Token.Typ T) => Syntax.pretty_typ ctxt T | SOME (Token.Term t) => Syntax.pretty_term ctxt t @@ -113,7 +115,7 @@ (* check *) -fun check_src ctxt table (Src {name = (xname, pos), args, output_info}) = +fun check_src ctxt table (Src {name = (xname, pos), args, output_info = _}) = let val (name, x) = Name_Space.check (Context.Proof ctxt) table (xname, pos); val space = Name_Space.space_of_table table; @@ -157,12 +159,15 @@ val string = token (Parse.string || Parse.verbatim); val alt_string = token Parse.alt_string; -val symbolic = token Parse.keyword_ident_or_symbolic; +val symbolic = token (Parse.keyword_with Token.ident_or_symbolic); fun $$$ x = (ident || token Parse.keyword) :|-- (fn tok => - let val y = Token.content_of tok - in if x = y then (Token.assign (SOME (Token.Literal x)) tok; Scan.succeed x) else Scan.fail end); + let val y = Token.content_of tok in + if x = y + then (Token.assign (SOME (Token.Literal Markup.quasi_keyword)) tok; Scan.succeed x) + else Scan.fail + end); val named = ident || string; @@ -317,7 +322,7 @@ val args1 = map Token.init_assignable args0; fun reported_text () = if Context_Position.is_visible_generic context then - maps (Token.reports_of_value o Token.closure) args1 + ((pos, Markup.operator) :: maps (Token.reports_of_value o Token.closure) args1) |> map (fn (p, m) => Position.reported_text p m "") |> implode else ""; diff -r 8ae2965ddc80 -r 38f13d055107 src/Pure/Isar/parse.ML --- a/src/Pure/Isar/parse.ML Wed Mar 12 14:37:14 2014 +0100 +++ b/src/Pure/Isar/parse.ML Wed Mar 12 16:11:47 2014 +0100 @@ -37,7 +37,6 @@ val eof: string parser val command_name: string -> string parser val keyword_with: (string -> bool) -> string parser - val keyword_ident_or_symbolic: string parser val $$$ : string -> string parser val reserved: string -> string parser val semicolon: string parser @@ -195,7 +194,6 @@ val eof = kind Token.EOF; fun keyword_with pred = RESET_VALUE (Scan.one (Token.keyword_with pred) >> Token.content_of); -val keyword_ident_or_symbolic = keyword_with Token.ident_or_symbolic; fun command_name x = group (fn () => Token.str_of_kind Token.Command ^ " " ^ quote x) @@ -204,7 +202,8 @@ fun $$$ x = group (fn () => Token.str_of_kind Token.Keyword ^ " " ^ quote x) - (keyword_with (fn y => x = y)); + (Scan.ahead not_eof -- keyword_with (fn y => x = y)) + >> (fn (tok, x) => (Token.assign (SOME (Token.Literal Markup.quasi_keyword)) tok; x)); fun reserved x = group (fn () => "reserved identifier " ^ quote x) @@ -270,7 +269,7 @@ val path = group (fn () => "file name/path specification") name; -val liberal_name = keyword_ident_or_symbolic || xname; +val liberal_name = keyword_with Token.ident_or_symbolic || xname; val parname = Scan.optional ($$$ "(" |-- name --| $$$ ")") ""; val parbinding = Scan.optional ($$$ "(" |-- binding --| $$$ ")") Binding.empty; diff -r 8ae2965ddc80 -r 38f13d055107 src/Pure/Isar/token.ML --- a/src/Pure/Isar/token.ML Wed Mar 12 14:37:14 2014 +0100 +++ b/src/Pure/Isar/token.ML Wed Mar 12 16:11:47 2014 +0100 @@ -12,7 +12,7 @@ Error of string | Sync | EOF type file = {src_path: Path.T, lines: string list, digest: SHA1.digest, pos: Position.T} datatype value = - Literal of string | Text of string | Typ of typ | Term of term | Fact of thm list | + Literal of Markup.T | Text of string | Typ of typ | Term of term | Fact of thm list | Attribute of morphism -> attribute | Files of file Exn.result list type T val str_of_kind: kind -> string @@ -42,7 +42,7 @@ val inner_syntax_of: T -> string val source_position_of: T -> Symbol_Pos.source val content_of: T -> string - val value_markup: value -> Markup.T list + val keyword_markup: Markup.T -> string -> Markup.T val completion_report: T -> Position.report_text list val report: T -> Position.report_text val markup: T -> Markup.T @@ -87,7 +87,7 @@ type file = {src_path: Path.T, lines: string list, digest: SHA1.digest, pos: Position.T}; datatype value = - Literal of string | + Literal of Markup.T | Text of string | Typ of typ | Term of term | @@ -253,15 +253,11 @@ | Sync => (Markup.control, "") | EOF => (Markup.control, ""); +in + fun keyword_markup keyword x = if Symbol.is_ascii_identifier x then keyword else Markup.operator; -in - -fun value_markup (Literal x) = - keyword_markup Markup.quasi_keyword x :: Completion.suppress_abbrevs x - | value_markup _ = []; - fun completion_report tok = if is_kind Keyword tok then map (fn m => ((pos_of tok, m), "")) (Completion.suppress_abbrevs (content_of tok)) @@ -332,10 +328,16 @@ fun reports_of_value tok = (case get_value tok of - NONE => [] - | SOME v => - let val pos = pos_of tok - in if Position.is_reported pos then map (pair pos) (value_markup v) else [] end); + SOME (Literal markup) => + let + val pos = pos_of tok; + val x = content_of tok; + in + if Position.is_reported pos then + map (pair pos) (keyword_markup markup x :: Completion.suppress_abbrevs x) + else [] + end + | _ => []); (* make values *) diff -r 8ae2965ddc80 -r 38f13d055107 src/Tools/jEdit/src/rendering.scala --- a/src/Tools/jEdit/src/rendering.scala Wed Mar 12 14:37:14 2014 +0100 +++ b/src/Tools/jEdit/src/rendering.scala Wed Mar 12 16:11:47 2014 +0100 @@ -653,6 +653,7 @@ Markup.KEYWORD2 -> keyword2_color, Markup.KEYWORD3 -> keyword3_color, Markup.QUASI_KEYWORD -> quasi_keyword_color, + Markup.OPERATOR -> Color.BLACK, Markup.STRING -> Color.BLACK, Markup.ALTSTRING -> Color.BLACK, Markup.VERBATIM -> Color.BLACK,