more markup for improper elements;
authorwenzelm
Tue Mar 18 12:25:17 2014 +0100 (2014-03-18 ago)
changeset 562020a11d17eeeff
parent 56201 dd2df97b379b
child 56203 76c72f4d0667
more markup for improper elements;
src/Pure/Isar/args.ML
src/Pure/Isar/parse.ML
src/Pure/Isar/proof_context.ML
src/Pure/Isar/token.ML
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
src/Tools/jEdit/etc/options
src/Tools/jEdit/src/rendering.scala
     1.1 --- a/src/Pure/Isar/args.ML	Tue Mar 18 11:27:09 2014 +0100
     1.2 +++ b/src/Pure/Isar/args.ML	Tue Mar 18 12:25:17 2014 +0100
     1.3 @@ -159,7 +159,7 @@
     1.4    (ident || Parse.token Parse.keyword) :|-- (fn tok =>
     1.5      let val y = Token.content_of tok in
     1.6        if x = y
     1.7 -      then (Token.assign (SOME (Token.Literal Markup.quasi_keyword)) tok; Scan.succeed x)
     1.8 +      then (Token.assign (SOME (Token.Literal (false, Markup.quasi_keyword))) tok; Scan.succeed x)
     1.9        else Scan.fail
    1.10      end);
    1.11  
    1.12 @@ -251,7 +251,7 @@
    1.13    Parse.nat >> (fn i => fn tac => tac i) ||
    1.14    $$$ "!" >> K ALLGOALS;
    1.15  
    1.16 -val goal = $$$ "[" |-- Parse.!!! (from_to --| $$$ "]");
    1.17 +val goal = Parse.keyword_improper "[" |-- Parse.!!! (from_to --| Parse.keyword_improper "]");
    1.18  fun goal_spec x = Scan.lift (Scan.optional goal (fn tac => tac 1)) x;
    1.19  
    1.20  
     2.1 --- a/src/Pure/Isar/parse.ML	Tue Mar 18 11:27:09 2014 +0100
     2.2 +++ b/src/Pure/Isar/parse.ML	Tue Mar 18 12:25:17 2014 +0100
     2.3 @@ -38,6 +38,8 @@
     2.4    val eof: string parser
     2.5    val command_name: string -> string parser
     2.6    val keyword_with: (string -> bool) -> string parser
     2.7 +  val keyword_markup: bool * Markup.T -> string -> string parser
     2.8 +  val keyword_improper: string -> string parser
     2.9    val $$$ : string -> string parser
    2.10    val reserved: string -> string parser
    2.11    val semicolon: string parser
    2.12 @@ -198,17 +200,20 @@
    2.13  val sync = kind Token.Sync;
    2.14  val eof = kind Token.EOF;
    2.15  
    2.16 -fun keyword_with pred = RESET_VALUE (Scan.one (Token.keyword_with pred) >> Token.content_of);
    2.17 -
    2.18  fun command_name x =
    2.19    group (fn () => Token.str_of_kind Token.Command ^ " " ^ quote x)
    2.20      (RESET_VALUE (Scan.one (fn tok => Token.is_command tok andalso Token.content_of tok = x)))
    2.21    >> Token.content_of;
    2.22  
    2.23 -fun $$$ x =
    2.24 +fun keyword_with pred = RESET_VALUE (Scan.one (Token.keyword_with pred) >> Token.content_of);
    2.25 +
    2.26 +fun keyword_markup markup x =
    2.27    group (fn () => Token.str_of_kind Token.Keyword ^ " " ^ quote x)
    2.28      (Scan.ahead not_eof -- keyword_with (fn y => x = y))
    2.29 -  >> (fn (tok, x) => (Token.assign (SOME (Token.Literal Markup.quasi_keyword)) tok; x));
    2.30 +  >> (fn (tok, x) => (Token.assign (SOME (Token.Literal markup)) tok; x));
    2.31 +
    2.32 +val keyword_improper = keyword_markup (true, Markup.improper);
    2.33 +val $$$ = keyword_markup (false, Markup.quasi_keyword);
    2.34  
    2.35  fun reserved x =
    2.36    group (fn () => "reserved identifier " ^ quote x)
     3.1 --- a/src/Pure/Isar/proof_context.ML	Tue Mar 18 11:27:09 2014 +0100
     3.2 +++ b/src/Pure/Isar/proof_context.ML	Tue Mar 18 12:25:17 2014 +0100
     3.3 @@ -1204,8 +1204,9 @@
     3.4  
     3.5  fun check_case ctxt (name, pos) fxs =
     3.6    let
     3.7 -    val (_, ((Rule_Cases.Case {fixes, assumes, binds, cases}, _), _)) =
     3.8 +    val (_, ((Rule_Cases.Case {fixes, assumes, binds, cases}, is_proper), _)) =
     3.9        Name_Space.check (Context.Proof ctxt) (cases_of ctxt) (name, pos);
    3.10 +    val _ = if is_proper then () else Context_Position.report ctxt pos Markup.improper;
    3.11  
    3.12      fun replace (opt_x :: xs) ((y, T) :: ys) = (the_default y opt_x, T) :: replace xs ys
    3.13        | replace [] ys = ys
     4.1 --- a/src/Pure/Isar/token.ML	Tue Mar 18 11:27:09 2014 +0100
     4.2 +++ b/src/Pure/Isar/token.ML	Tue Mar 18 12:25:17 2014 +0100
     4.3 @@ -12,7 +12,7 @@
     4.4      Error of string | Sync | EOF
     4.5    type file = {src_path: Path.T, lines: string list, digest: SHA1.digest, pos: Position.T}
     4.6    datatype value =
     4.7 -    Literal of Markup.T | Text of string | Typ of typ | Term of term | Fact of thm list |
     4.8 +    Literal of bool * Markup.T | Text of string | Typ of typ | Term of term | Fact of thm list |
     4.9      Attribute of morphism -> attribute | Files of file Exn.result list
    4.10    type T
    4.11    val str_of_kind: kind -> string
    4.12 @@ -42,7 +42,7 @@
    4.13    val inner_syntax_of: T -> string
    4.14    val source_position_of: T -> Symbol_Pos.source
    4.15    val content_of: T -> string
    4.16 -  val keyword_markup: Markup.T -> string -> Markup.T
    4.17 +  val keyword_markup: bool * Markup.T -> string -> Markup.T
    4.18    val completion_report: T -> Position.report_text list
    4.19    val report: T -> Position.report_text
    4.20    val markup: T -> Markup.T
    4.21 @@ -87,7 +87,7 @@
    4.22  type file = {src_path: Path.T, lines: string list, digest: SHA1.digest, pos: Position.T};
    4.23  
    4.24  datatype value =
    4.25 -  Literal of Markup.T |
    4.26 +  Literal of bool * Markup.T |
    4.27    Text of string |
    4.28    Typ of typ |
    4.29    Term of term |
    4.30 @@ -255,8 +255,8 @@
    4.31  
    4.32  in
    4.33  
    4.34 -fun keyword_markup keyword x =
    4.35 -  if Symbol.is_ascii_identifier x then keyword else Markup.delimiter;
    4.36 +fun keyword_markup (important, keyword) x =
    4.37 +  if important orelse Symbol.is_ascii_identifier x then keyword else Markup.delimiter;
    4.38  
    4.39  fun completion_report tok =
    4.40    if is_kind Keyword tok
    4.41 @@ -265,7 +265,7 @@
    4.42  
    4.43  fun report tok =
    4.44    if is_kind Keyword tok then
    4.45 -    ((pos_of tok, keyword_markup Markup.keyword2 (content_of tok)), "")
    4.46 +    ((pos_of tok, keyword_markup (false, Markup.keyword2) (content_of tok)), "")
    4.47    else
    4.48      let val (m, text) = token_kind_markup (kind_of tok)
    4.49      in ((pos_of tok, m), text) end;
     5.1 --- a/src/Pure/PIDE/markup.ML	Tue Mar 18 11:27:09 2014 +0100
     5.2 +++ b/src/Pure/PIDE/markup.ML	Tue Mar 18 12:25:17 2014 +0100
     5.3 @@ -105,7 +105,6 @@
     5.4    val paragraphN: string val paragraph: T
     5.5    val text_foldN: string val text_fold: T
     5.6    val commandN: string val command: T
     5.7 -  val operatorN: string val operator: T
     5.8    val stringN: string val string: T
     5.9    val altstringN: string val altstring: T
    5.10    val verbatimN: string val verbatim: T
    5.11 @@ -117,6 +116,8 @@
    5.12    val keyword2N: string val keyword2: T
    5.13    val keyword3N: string val keyword3: T
    5.14    val quasi_keywordN: string val quasi_keyword: T
    5.15 +  val improperN: string val improper: T
    5.16 +  val operatorN: string val operator: T
    5.17    val elapsedN: string
    5.18    val cpuN: string
    5.19    val gcN: string
    5.20 @@ -427,6 +428,7 @@
    5.21  val (keyword2N, keyword2) = markup_elem "keyword2";
    5.22  val (keyword3N, keyword3) = markup_elem "keyword3";
    5.23  val (quasi_keywordN, quasi_keyword) = markup_elem "quasi_keyword";
    5.24 +val (improperN, improper) = markup_elem "improper";
    5.25  val (operatorN, operator) = markup_elem "operator";
    5.26  val (stringN, string) = markup_elem "string";
    5.27  val (altstringN, altstring) = markup_elem "altstring";
     6.1 --- a/src/Pure/PIDE/markup.scala	Tue Mar 18 11:27:09 2014 +0100
     6.2 +++ b/src/Pure/PIDE/markup.scala	Tue Mar 18 12:25:17 2014 +0100
     6.3 @@ -216,6 +216,7 @@
     6.4    val KEYWORD2 = "keyword2"
     6.5    val KEYWORD3 = "keyword3"
     6.6    val QUASI_KEYWORD = "quasi_keyword"
     6.7 +  val IMPROPER = "improper"
     6.8    val OPERATOR = "operator"
     6.9    val STRING = "string"
    6.10    val ALTSTRING = "altstring"
     7.1 --- a/src/Tools/jEdit/etc/options	Tue Mar 18 11:27:09 2014 +0100
     7.2 +++ b/src/Tools/jEdit/etc/options	Tue Mar 18 12:25:17 2014 +0100
     7.3 @@ -82,6 +82,7 @@
     7.4  option keyword2_color : string = "009966FF"
     7.5  option keyword3_color : string = "0099FFFF"
     7.6  option quasi_keyword_color : string = "9966FFFF"
     7.7 +option improper_color : string = "FF5050FF"
     7.8  option operator_color : string = "323232FF"
     7.9  option caret_invisible_color : string = "50000080"
    7.10  option completion_color : string = "0000FFFF"
     8.1 --- a/src/Tools/jEdit/src/rendering.scala	Tue Mar 18 11:27:09 2014 +0100
     8.2 +++ b/src/Tools/jEdit/src/rendering.scala	Tue Mar 18 12:25:17 2014 +0100
     8.3 @@ -239,6 +239,7 @@
     8.4    val keyword2_color = color_value("keyword2_color")
     8.5    val keyword3_color = color_value("keyword3_color")
     8.6    val quasi_keyword_color = color_value("quasi_keyword_color")
     8.7 +  val improper_color = color_value("improper_color")
     8.8    val operator_color = color_value("operator_color")
     8.9    val caret_invisible_color = color_value("caret_invisible_color")
    8.10    val completion_color = color_value("completion_color")
    8.11 @@ -654,6 +655,7 @@
    8.12        Markup.KEYWORD2 -> keyword2_color,
    8.13        Markup.KEYWORD3 -> keyword3_color,
    8.14        Markup.QUASI_KEYWORD -> quasi_keyword_color,
    8.15 +      Markup.IMPROPER -> improper_color,
    8.16        Markup.OPERATOR -> operator_color,
    8.17        Markup.STRING -> Color.BLACK,
    8.18        Markup.ALTSTRING -> Color.BLACK,