clarified init_assignable: make double-sure that initial values are reset;
authorwenzelm
Wed Mar 05 13:11:08 2014 +0100 (2014-03-05)
changeset 55914c5b752d549e3
parent 55913 c1409c103b77
child 55915 607948c90bf0
clarified init_assignable: make double-sure that initial values are reset;
more systematic reports for Args.syntax: indicate Args.$$$ quasi-keywords and suppress confusing completion of single symbols like ":", "|", "?";
src/Pure/General/completion.scala
src/Pure/Isar/args.ML
src/Pure/Isar/attrib.ML
src/Pure/Isar/element.ML
src/Pure/Isar/token.ML
src/Pure/ML/ml_thms.ML
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
src/Tools/jEdit/src/completion_popup.scala
src/Tools/jEdit/src/rendering.scala
     1.1 --- a/src/Pure/General/completion.scala	Wed Mar 05 09:59:48 2014 +0100
     1.2 +++ b/src/Pure/General/completion.scala	Wed Mar 05 13:11:08 2014 +0100
     1.3 @@ -27,6 +27,11 @@
     1.4      immediate: Boolean)
     1.5    { override def toString: String = description }
     1.6  
     1.7 +  object Result
     1.8 +  {
     1.9 +    def empty(range: Text.Range): Result = Result(range, "", false, Nil)
    1.10 +  }
    1.11 +
    1.12    sealed case class Result(
    1.13      range: Text.Range,
    1.14      original: String,
    1.15 @@ -136,6 +141,8 @@
    1.16                Some(Names(info.range, total, names))
    1.17              }
    1.18              catch { case _: XML.Error => None }
    1.19 +          case XML.Elem(Markup(Markup.NO_COMPLETION, _), _) =>
    1.20 +            Some(Names(info.range, 0, Nil))
    1.21            case _ => None
    1.22          }
    1.23      }
    1.24 @@ -143,6 +150,8 @@
    1.25  
    1.26    sealed case class Names(range: Text.Range, total: Int, names: List[(String, String)])
    1.27    {
    1.28 +    def no_completion: Boolean = total == 0 && names.isEmpty
    1.29 +
    1.30      def complete(
    1.31        history: Completion.History,
    1.32        decode: Boolean,
     2.1 --- a/src/Pure/Isar/args.ML	Wed Mar 05 09:59:48 2014 +0100
     2.2 +++ b/src/Pure/Isar/args.ML	Wed Mar 05 13:11:08 2014 +0100
     2.3 @@ -13,7 +13,7 @@
     2.4    val pretty_src: Proof.context -> src -> Pretty.T
     2.5    val map_name: (string -> string) -> src -> src
     2.6    val transform_values: morphism -> src -> src
     2.7 -  val assignable: src -> src
     2.8 +  val init_assignable: src -> src
     2.9    val closure: src -> src
    2.10    val context: Proof.context context_parser
    2.11    val theory: theory context_parser
    2.12 @@ -85,7 +85,8 @@
    2.13      val prt_thm = Pretty.backquote o Display.pretty_thm ctxt;
    2.14      fun prt arg =
    2.15        (case Token.get_value arg of
    2.16 -        SOME (Token.Text s) => Pretty.str (quote s)
    2.17 +        SOME (v as Token.Literal s) => Pretty.marks_str (Token.value_markup false v, s)
    2.18 +      | SOME (Token.Text s) => Pretty.str (quote s)
    2.19        | SOME (Token.Typ T) => Syntax.pretty_typ ctxt T
    2.20        | SOME (Token.Term t) => Syntax.pretty_term ctxt t
    2.21        | SOME (Token.Fact ths) => Pretty.enclose "(" ")" (Pretty.breaks (map prt_thm ths))
    2.22 @@ -100,14 +101,13 @@
    2.23  (* values *)
    2.24  
    2.25  fun transform_values phi = map_args (Token.map_value
    2.26 -  (fn Token.Text s => Token.Text s
    2.27 -    | Token.Typ T => Token.Typ (Morphism.typ phi T)
    2.28 +  (fn Token.Typ T => Token.Typ (Morphism.typ phi T)
    2.29      | Token.Term t => Token.Term (Morphism.term phi t)
    2.30      | Token.Fact ths => Token.Fact (Morphism.fact phi ths)
    2.31      | Token.Attribute att => Token.Attribute (Morphism.transform phi att)
    2.32 -    | tok as Token.Files _ => tok));
    2.33 +    | tok => tok));
    2.34  
    2.35 -val assignable = map_args Token.assignable;
    2.36 +val init_assignable = map_args Token.init_assignable;
    2.37  val closure = map_args Token.closure;
    2.38  
    2.39  
    2.40 @@ -132,8 +132,10 @@
    2.41  val alt_string = token Parse.alt_string;
    2.42  val symbolic = token Parse.keyword_ident_or_symbolic;
    2.43  
    2.44 -fun $$$ x = (ident >> Token.content_of || Parse.keyword)
    2.45 -  :|-- (fn y => if x = y then Scan.succeed x else Scan.fail);
    2.46 +fun $$$ x =
    2.47 +  (ident || token Parse.keyword) :|-- (fn tok =>
    2.48 +    let val y = Token.content_of tok
    2.49 +    in if x = y then (Token.assign (SOME (Token.Literal x)) tok; Scan.succeed x) else Scan.fail end);
    2.50  
    2.51  
    2.52  val named = ident || string;
    2.53 @@ -287,13 +289,25 @@
    2.54  
    2.55  (** syntax wrapper **)
    2.56  
    2.57 -fun syntax kind scan (Src ((s, args), pos)) st =
    2.58 -  (case Scan.error (Scan.finite' Token.stopper (Scan.option scan)) (st, args) of
    2.59 -    (SOME x, (st', [])) => (x, st')
    2.60 -  | (_, (_, args')) =>
    2.61 -      error ("Bad arguments for " ^ kind ^ " " ^ quote s ^ Position.here pos ^
    2.62 -        (if null args' then "" else ":\n  " ^ space_implode " " (map Token.print args'))));
    2.63 +fun syntax kind scan (Src ((s, args0), pos)) context =
    2.64 +  let
    2.65 +    val args1 = map Token.init_assignable args0;
    2.66 +    fun reported_text () =
    2.67 +      if Context_Position.is_visible_generic context then
    2.68 +        maps (Token.reports_of_value o Token.closure) args1
    2.69 +        |> map (fn (p, m) => Position.reported_text p m "")
    2.70 +        |> implode
    2.71 +      else "";
    2.72 +  in
    2.73 +    (case Scan.error (Scan.finite' Token.stopper (Scan.option scan)) (context, args1) of
    2.74 +      (SOME x, (context', [])) => (Output.report (reported_text ()); (x, context'))
    2.75 +    | (_, (_, args2)) =>
    2.76 +        error ("Bad arguments for " ^ kind ^ " " ^ quote s ^ Position.here pos ^
    2.77 +          (if null args2 then "" else ":\n  " ^ space_implode " " (map Token.print args2)) ^
    2.78 +          Markup.markup Markup.report (reported_text ())))
    2.79 +  end;
    2.80  
    2.81 -fun context_syntax kind scan src = apsnd Context.the_proof o syntax kind scan src o Context.Proof;
    2.82 +fun context_syntax kind scan src =
    2.83 +  apsnd Context.the_proof o syntax kind scan src o Context.Proof;
    2.84  
    2.85  end;
     3.1 --- a/src/Pure/Isar/attrib.ML	Wed Mar 05 09:59:48 2014 +0100
     3.2 +++ b/src/Pure/Isar/attrib.ML	Wed Mar 05 13:11:08 2014 +0100
     3.3 @@ -262,7 +262,7 @@
     3.4  
     3.5  fun apply_att src (context, th) =
     3.6    let
     3.7 -    val src1 = Args.assignable src;
     3.8 +    val src1 = Args.init_assignable src;
     3.9      val result = attribute_generic context src1 (context, th);
    3.10      val src2 = Args.closure src1;
    3.11    in (src2, result) end;
     4.1 --- a/src/Pure/Isar/element.ML	Wed Mar 05 09:59:48 2014 +0100
     4.2 +++ b/src/Pure/Isar/element.ML	Wed Mar 05 13:11:08 2014 +0100
     4.3 @@ -512,7 +512,7 @@
     4.4  fun activate_i elem ctxt =
     4.5    let
     4.6      val elem' =
     4.7 -      (case map_ctxt_attrib Args.assignable elem of
     4.8 +      (case map_ctxt_attrib Args.init_assignable elem of
     4.9          Defines defs =>
    4.10            Defines (defs |> map (fn ((a, atts), (t, ps)) =>
    4.11              ((Thm.def_binding_optional (Binding.name (#1 (#1 (Local_Defs.cert_def ctxt t)))) a, atts),
     5.1 --- a/src/Pure/Isar/token.ML	Wed Mar 05 09:59:48 2014 +0100
     5.2 +++ b/src/Pure/Isar/token.ML	Wed Mar 05 13:11:08 2014 +0100
     5.3 @@ -12,7 +12,7 @@
     5.4      Error of string | Sync | EOF
     5.5    type file = {src_path: Path.T, lines: string list, digest: SHA1.digest, pos: Position.T}
     5.6    datatype value =
     5.7 -    Text of string | Typ of typ | Term of term | Fact of thm list |
     5.8 +    Literal of string | Text of string | Typ of typ | Term of term | Fact of thm list |
     5.9      Attribute of morphism -> attribute | Files of file Exn.result list
    5.10    type T
    5.11    val str_of_kind: kind -> string
    5.12 @@ -43,6 +43,7 @@
    5.13    val source_position_of: T -> Symbol_Pos.source
    5.14    val content_of: T -> string
    5.15    val markup: T -> Markup.T * string
    5.16 +  val value_markup: bool -> value -> Markup.T list
    5.17    val unparse: T -> string
    5.18    val print: T -> string
    5.19    val text_of: T -> string * string
    5.20 @@ -50,12 +51,13 @@
    5.21    val put_files: file Exn.result list -> T -> T
    5.22    val get_value: T -> value option
    5.23    val map_value: (value -> value) -> T -> T
    5.24 +  val reports_of_value: T -> Position.report list
    5.25    val mk_text: string -> T
    5.26    val mk_typ: typ -> T
    5.27    val mk_term: term -> T
    5.28    val mk_fact: thm list -> T
    5.29    val mk_attribute: (morphism -> attribute) -> T
    5.30 -  val assignable: T -> T
    5.31 +  val init_assignable: T -> T
    5.32    val assign: value option -> T -> unit
    5.33    val closure: T -> T
    5.34    val ident_or_symbolic: string -> bool
    5.35 @@ -83,6 +85,7 @@
    5.36  type file = {src_path: Path.T, lines: string list, digest: SHA1.digest, pos: Position.T};
    5.37  
    5.38  datatype value =
    5.39 +  Literal of string |
    5.40    Text of string |
    5.41    Typ of typ |
    5.42    Term of term |
    5.43 @@ -248,13 +251,24 @@
    5.44    | Sync          => (Markup.control, "")
    5.45    | EOF           => (Markup.control, "");
    5.46  
    5.47 +fun keyword_markup x =
    5.48 +  if Symbol.is_ascii_identifier x
    5.49 +  then Markup.keyword2
    5.50 +  else Markup.operator;
    5.51 +
    5.52  in
    5.53  
    5.54  fun markup tok =
    5.55 -  if keyword_with (not o Symbol.is_ascii_identifier) tok
    5.56 -  then (Markup.operator, "")
    5.57 +  if is_kind Keyword tok
    5.58 +  then (keyword_markup (content_of tok), "")
    5.59    else token_kind_markup (kind_of tok);
    5.60  
    5.61 +fun value_markup known_keyword (Literal x) =
    5.62 +      (if known_keyword then [] else [keyword_markup x]) @
    5.63 +      (if Symbol.is_ascii_identifier x orelse length (Symbol.explode x) > 1 then []
    5.64 +       else [Markup.no_completion])
    5.65 +  | value_markup _ _ = [];
    5.66 +
    5.67  end;
    5.68  
    5.69  
    5.70 @@ -309,6 +323,18 @@
    5.71  fun map_value f (Token (x, y, Value (SOME v))) = Token (x, y, Value (SOME (f v)))
    5.72    | map_value _ tok = tok;
    5.73  
    5.74 +fun reports_of_value tok =
    5.75 +  (case get_value tok of
    5.76 +    NONE => []
    5.77 +  | SOME v =>
    5.78 +      let
    5.79 +        val pos = pos_of tok;
    5.80 +        val known_keyword = is_kind Keyword tok;
    5.81 +      in
    5.82 +        if Position.is_reported pos then map (pair pos) (value_markup known_keyword v)
    5.83 +        else []
    5.84 +      end);
    5.85 +
    5.86  
    5.87  (* make values *)
    5.88  
    5.89 @@ -323,9 +349,10 @@
    5.90  
    5.91  (* static binding *)
    5.92  
    5.93 -(*1st stage: make empty slots assignable*)
    5.94 -fun assignable (Token (x, y, Slot)) = Token (x, y, Assignable (Unsynchronized.ref NONE))
    5.95 -  | assignable tok = tok;
    5.96 +(*1st stage: initialize assignable slots*)
    5.97 +fun init_assignable (Token (x, y, Slot)) = Token (x, y, Assignable (Unsynchronized.ref NONE))
    5.98 +  | init_assignable (tok as Token (_, _, Assignable r)) = (r := NONE; tok)
    5.99 +  | init_assignable tok = tok;
   5.100  
   5.101  (*2nd stage: assign values as side-effect of scanning*)
   5.102  fun assign v (Token (_, _, Assignable r)) = r := v
     6.1 --- a/src/Pure/ML/ml_thms.ML	Wed Mar 05 09:59:48 2014 +0100
     6.2 +++ b/src/Pure/ML/ml_thms.ML	Wed Mar 05 13:11:08 2014 +0100
     6.3 @@ -90,17 +90,13 @@
     6.4  val _ = Theory.setup
     6.5    (ML_Context.add_antiq @{binding lemma}
     6.6      (Scan.depend (fn context =>
     6.7 -      Args.mode "open" -- Parse.enum1_positions "and" (Scan.repeat1 goal) --
     6.8 -      Parse.position by -- Method.parse -- Scan.option Method.parse
     6.9 -     >> (fn ((((is_open, (raw_propss, and_positions)), (_, by_pos)), m1), m2) =>
    6.10 +      Args.mode "open" -- Parse.enum1 "and" (Scan.repeat1 goal) --
    6.11 +      (by |-- Method.parse -- Scan.option Method.parse)
    6.12 +     >> (fn ((is_open, raw_propss), (m1, m2)) =>
    6.13            let
    6.14              val ctxt = Context.proof_of context;
    6.15  
    6.16 -            val reports =
    6.17 -              (by_pos, Markup.keyword1) ::
    6.18 -                map (rpair Markup.keyword2) and_positions @
    6.19 -                maps Method.reports_of (m1 :: the_list m2);
    6.20 -            val _ = Context_Position.reports ctxt reports;
    6.21 +            val _ = Context_Position.reports ctxt (maps Method.reports_of (m1 :: the_list m2));
    6.22  
    6.23              val propss = burrow (map (rpair []) o Syntax.read_props ctxt) raw_propss;
    6.24              val prep_result = Goal.norm_result ctxt #> not is_open ? Thm.close_derivation;
     7.1 --- a/src/Pure/PIDE/markup.ML	Wed Mar 05 09:59:48 2014 +0100
     7.2 +++ b/src/Pure/PIDE/markup.ML	Wed Mar 05 13:11:08 2014 +0100
     7.3 @@ -42,6 +42,7 @@
     7.4    val defN: string
     7.5    val refN: string
     7.6    val completionN: string val completion: T
     7.7 +  val no_completionN: string val no_completion: T
     7.8    val lineN: string
     7.9    val offsetN: string
    7.10    val end_offsetN: string
    7.11 @@ -304,6 +305,7 @@
    7.12  (* completion *)
    7.13  
    7.14  val (completionN, completion) = markup_elem "completion";
    7.15 +val (no_completionN, no_completion) = markup_elem "no_completion";
    7.16  
    7.17  
    7.18  (* position *)
     8.1 --- a/src/Pure/PIDE/markup.scala	Wed Mar 05 09:59:48 2014 +0100
     8.2 +++ b/src/Pure/PIDE/markup.scala	Wed Mar 05 13:11:08 2014 +0100
     8.3 @@ -70,6 +70,7 @@
     8.4    /* completion */
     8.5  
     8.6    val COMPLETION = "completion"
     8.7 +  val NO_COMPLETION = "no_completion"
     8.8  
     8.9  
    8.10    /* position */
     9.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Wed Mar 05 09:59:48 2014 +0100
     9.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Wed Mar 05 13:11:08 2014 +0100
     9.3 @@ -114,7 +114,9 @@
     9.4              before_caret_range(rendering).try_restrict(line_range) match {
     9.5                case Some(range) if !range.is_singularity =>
     9.6                  rendering.completion_names(range) match {
     9.7 -                  case Some(names) => Some(names.range)
     9.8 +                  case Some(names) =>
     9.9 +                    if (names.no_completion) None
    9.10 +                    else Some(names.range)
    9.11                    case None =>
    9.12                      syntax_completion(false, Some(rendering)) match {
    9.13                        case Some(result) => Some(result.range)
    9.14 @@ -232,12 +234,15 @@
    9.15              case Some(doc_view) =>
    9.16                val rendering = doc_view.get_rendering()
    9.17                rendering.completion_names(before_caret_range(rendering)) match {
    9.18 +                case Some(names) =>
    9.19 +                  if (names.no_completion)
    9.20 +                    Some(Completion.Result.empty(names.range))
    9.21 +                  else
    9.22 +                    JEdit_Lib.try_get_text(buffer, names.range) match {
    9.23 +                      case Some(original) => names.complete(history, decode, original)
    9.24 +                      case None => None
    9.25 +                    }
    9.26                  case None => None
    9.27 -                case Some(names) =>
    9.28 -                  JEdit_Lib.try_get_text(buffer, names.range) match {
    9.29 -                    case Some(original) => names.complete(history, decode, original)
    9.30 -                    case None => None
    9.31 -                  }
    9.32                }
    9.33              case None => None
    9.34            }
    10.1 --- a/src/Tools/jEdit/src/rendering.scala	Wed Mar 05 09:59:48 2014 +0100
    10.2 +++ b/src/Tools/jEdit/src/rendering.scala	Wed Mar 05 13:11:08 2014 +0100
    10.3 @@ -130,7 +130,7 @@
    10.4    /* markup elements */
    10.5  
    10.6    private val completion_names_elements =
    10.7 -    Document.Elements(Markup.COMPLETION)
    10.8 +    Document.Elements(Markup.COMPLETION, Markup.NO_COMPLETION)
    10.9  
   10.10    private val completion_language_elements =
   10.11      Document.Elements(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM,