# HG changeset patch # User wenzelm # Date 1393365261 -3600 # Node ID c90cc76ec8558b5dfc28eb8f41849090c1ec7093 # Parent 30312334445923310ad206107693d5efd310d360# Parent 43d0e2a34c9d36e8ccd981e08ade6cb088869eda merged diff -r 303123344459 -r c90cc76ec855 src/Doc/antiquote_setup.ML --- a/src/Doc/antiquote_setup.ML Tue Feb 25 19:07:42 2014 +0100 +++ b/src/Doc/antiquote_setup.ML Tue Feb 25 22:54:21 2014 +0100 @@ -156,8 +156,6 @@ val _ = List.app (Position.report pos) markup; in true end; -fun thy_check check ctxt = can (check (Proof_Context.theory_of ctxt)); - fun check_tool (name, pos) = let fun tool dir = @@ -212,19 +210,19 @@ entity_antiqs (K command_check) "isacommand" "command" #> entity_antiqs (K (Keyword.is_keyword o #1)) "isakeyword" "keyword" #> entity_antiqs (K (Keyword.is_keyword o #1)) "isakeyword" "element" #> - entity_antiqs (thy_check Method.check) "" "method" #> - entity_antiqs (thy_check Attrib.check) "" "attribute" #> + entity_antiqs (can o Method.check_name) "" "method" #> + entity_antiqs (can o Attrib.check o Proof_Context.theory_of) "" "attribute" #> entity_antiqs no_check "" "fact" #> entity_antiqs no_check "" "variable" #> entity_antiqs no_check "" "case" #> - entity_antiqs (thy_check Thy_Output.check_command) "" "antiquotation" #> - entity_antiqs (thy_check Thy_Output.check_option) "" "antiquotation option" #> + entity_antiqs (can o Thy_Output.check_command) "" "antiquotation" #> + entity_antiqs (can o Thy_Output.check_option) "" "antiquotation option" #> entity_antiqs no_check "isatt" "setting" #> entity_antiqs no_check "isatt" "system option" #> entity_antiqs no_check "" "inference" #> entity_antiqs no_check "isatt" "executable" #> entity_antiqs (K check_tool) "isatool" "tool" #> - entity_antiqs (thy_check ML_Context.check_antiq) "" Markup.ML_antiquotationN; + entity_antiqs (can o ML_Context.check_antiq) "" Markup.ML_antiquotationN; end; diff -r 303123344459 -r c90cc76ec855 src/HOL/Multivariate_Analysis/Integration.thy --- a/src/HOL/Multivariate_Analysis/Integration.thy Tue Feb 25 19:07:42 2014 +0100 +++ b/src/HOL/Multivariate_Analysis/Integration.thy Tue Feb 25 22:54:21 2014 +0100 @@ -2158,12 +2158,19 @@ done qed qed - then guess f + then obtain f where f: + "\x. + \ P {fst x..snd x} \ + \ P {fst (f x)..snd (f x)} \ + (\i\Basis. + fst x \ i \ fst (f x) \ i \ + fst (f x) \ i \ snd (f x) \ i \ + snd (f x) \ i \ snd x \ i \ + 2 * (snd (f x) \ i - fst (f x) \ i) \ snd x \ i - fst x \ i)" apply - apply (drule choice) - apply (erule exE) - done - note f = this + apply blast + done def AB \ "\n. (f ^^ n) (a,b)" def A \ "\n. fst(AB n)" def B \ "\n. snd(AB n)" @@ -2300,7 +2307,14 @@ then show thesis .. next assume as: "\ (\p. p tagged_division_of {a..b} \ g fine p)" - guess x + obtain x where x: + "x \ {a..b}" + "\e. 0 < e \ + \c d. + x \ {c..d} \ + {c..d} \ ball x e \ + {c..d} \ {a..b} \ + \ (\p. p tagged_division_of {c..d} \ g fine p)" apply (rule interval_bisection[of "\s. \p. p tagged_division_of s \ g fine p",rule_format,OF _ _ as]) apply (rule_tac x="{}" in exI) defer @@ -2320,7 +2334,7 @@ apply (rule fine_union) apply auto done - qed note x = this + qed blast obtain e where e: "e > 0" "ball x e \ g x" using gaugeD[OF assms, of x] unfolding open_contains_ball by auto from x(2)[OF e(1)] obtain c d where c_d: @@ -2354,9 +2368,20 @@ case goal1 let ?e = "norm (k1 - k2) / 2" from goal1(3) have e: "?e > 0" by auto - guess d1 by (rule has_integralD[OF goal1(1) e]) note d1=this - guess d2 by (rule has_integralD[OF goal1(2) e]) note d2=this - guess p by (rule fine_division_exists[OF gauge_inter[OF d1(1) d2(1)],of a b]) note p=this + obtain d1 where d1: + "gauge d1" + "\p. p tagged_division_of {a..b} \ + d1 fine p \ norm ((\(x, k)\p. content k *\<^sub>R f x) - k1) < norm (k1 - k2) / 2" + by (rule has_integralD[OF goal1(1) e]) blast + obtain d2 where d2: + "gauge d2" + "\p. p tagged_division_of {a..b} \ + d2 fine p \ norm ((\(x, k)\p. content k *\<^sub>R f x) - k2) < norm (k1 - k2) / 2" + by (rule has_integralD[OF goal1(2) e]) blast + obtain p where p: + "p tagged_division_of {a..b}" + "(\x. d1 x \ d2 x) fine p" + by (rule fine_division_exists[OF gauge_inter[OF d1(1) d2(1)]]) let ?c = "(\(x, k)\p. content k *\<^sub>R f x)" have "norm (k1 - k2) \ norm (?c - k2) + norm (?c - k1)" using norm_triangle_ineq4[of "k1 - ?c" "k2 - ?c"] @@ -2379,8 +2404,18 @@ done } assume as: "\ (\a b. i = {a..b})" - guess B1 by (rule has_integral_altD[OF assms(1) as,OF e]) note B1=this[rule_format] - guess B2 by (rule has_integral_altD[OF assms(2) as,OF e]) note B2=this[rule_format] + obtain B1 where B1: + "0 < B1" + "\a b. ball 0 B1 \ {a..b} \ + \z. ((\x. if x \ i then f x else 0) has_integral z) {a..b} \ + norm (z - k1) < norm (k1 - k2) / 2" + by (rule has_integral_altD[OF assms(1) as,OF e]) blast + obtain B2 where B2: + "0 < B2" + "\a b. ball 0 B2 \ {a..b} \ + \z. ((\x. if x \ i then f x else 0) has_integral z) {a..b} \ + norm (z - k2) < norm (k1 - k2) / 2" + by (rule has_integral_altD[OF assms(2) as,OF e]) blast have "\a b::'n. ball 0 B1 \ ball 0 B2 \ {a..b}" apply (rule bounded_subset_closed_interval) using bounded_Un bounded_ball @@ -2718,8 +2753,18 @@ case goal1 then have *: "e/2 > 0" by auto - from has_integral_altD[OF assms(1) as *] guess B1 . note B1=this[rule_format] - from has_integral_altD[OF assms(2) as *] guess B2 . note B2=this[rule_format] + from has_integral_altD[OF assms(1) as *] + obtain B1 where B1: + "0 < B1" + "\a b. ball 0 B1 \ {a..b} \ + \z. ((\x. if x \ s then f x else 0) has_integral z) {a..b} \ norm (z - k) < e / 2" + by blast + from has_integral_altD[OF assms(2) as *] + obtain B2 where B2: + "0 < B2" + "\a b. ball 0 B2 \ {a..b} \ + \z. ((\x. if x \ s then g x else 0) has_integral z) {a..b} \ norm (z - l) < e / 2" + by blast show ?case apply (rule_tac x="max B1 B2" in exI) apply rule diff -r 303123344459 -r c90cc76ec855 src/HOL/Tools/try0.ML --- a/src/HOL/Tools/try0.ML Tue Feb 25 19:07:42 2014 +0100 +++ b/src/HOL/Tools/try0.ML Tue Feb 25 22:54:21 2014 +0100 @@ -55,9 +55,10 @@ #> Scan.read Token.stopper Method.parse #> (fn SOME (Method.Source src, _) => src | _ => raise Fail "expected Source"); -fun apply_named_method_on_first_goal thy = +fun apply_named_method_on_first_goal ctxt = parse_method - #> Method.method thy + #> Method.check_source ctxt + #> Method.the_method ctxt #> Method.Basic #> curry Method.Select_Goals 1 #> Proof.refine; @@ -77,7 +78,7 @@ ((name ^ attrs |> attrs <> "" ? enclose "(" ")") ^ (if all_goals andalso nprems_of (#goal (Proof.goal st)) > 1 then "[1]" else "")) I (#goal o Proof.goal) - (apply_named_method_on_first_goal (Proof.theory_of st) (name ^ attrs)) st + (apply_named_method_on_first_goal (Proof.context_of st) (name ^ attrs)) st end else NONE; diff -r 303123344459 -r c90cc76ec855 src/Pure/General/completion.scala --- a/src/Pure/General/completion.scala Tue Feb 25 19:07:42 2014 +0100 +++ b/src/Pure/General/completion.scala Tue Feb 25 22:54:21 2014 +0100 @@ -166,15 +166,15 @@ /* language context */ - object Context + object Language_Context { - val outer = Context("", true, false) - val inner = Context(Markup.Language.UNKNOWN, true, false) - val ML_outer = Context(Markup.Language.ML, false, true) - val ML_inner = Context(Markup.Language.ML, true, false) + val outer = Language_Context("", true, false) + val inner = Language_Context(Markup.Language.UNKNOWN, true, false) + val ML_outer = Language_Context(Markup.Language.ML, false, true) + val ML_inner = Language_Context(Markup.Language.ML, true, false) } - sealed case class Context(language: String, symbols: Boolean, antiquotes: Boolean) + sealed case class Language_Context(language: String, symbols: Boolean, antiquotes: Boolean) { def is_outer: Boolean = language == "" } @@ -188,6 +188,12 @@ /* word parsers */ + def word_context(text: Option[String]): Boolean = + text match { + case None => false + case Some(s) => Word_Parsers.is_word(s) + } + private object Word_Parsers extends RegexParsers { override val whiteSpace = "".r @@ -274,7 +280,8 @@ explicit: Boolean, text_start: Text.Offset, text: CharSequence, - context: Completion.Context): Option[Completion.Result] = + word_context: Boolean, + language_context: Completion.Language_Context): Option[Completion.Result] = { val abbrevs_result = Scan.Parsers.parse(Scan.Parsers.literal(abbrevs_lex), new Library.Reverse(text)) match { @@ -284,8 +291,8 @@ case Nil => None case (a, _) :: _ => val ok = - if (a == Completion.antiquote) context.antiquotes - else context.symbols || Completion.default_abbrs.isDefinedAt(a) + if (a == Completion.antiquote) language_context.antiquotes + else language_context.symbols || Completion.default_abbrs.isDefinedAt(a) if (ok) Some((a, abbrevs.map(_._2))) else None } case _ => None @@ -293,18 +300,20 @@ val words_result = abbrevs_result orElse { - Completion.Word_Parsers.read(explicit, text) match { - case Some(word) => - val completions = - for { - s <- words_lex.completions(word) - if (if (keywords(s)) context.is_outer else context.symbols) - r <- words_map.get_list(s) - } yield r - if (completions.isEmpty) None - else Some(word, completions) - case None => None - } + if (word_context) None + else + Completion.Word_Parsers.read(explicit, text) match { + case Some(word) => + val completions = + for { + s <- words_lex.completions(word) + if (if (keywords(s)) language_context.is_outer else language_context.symbols) + r <- words_map.get_list(s) + } yield r + if (completions.isEmpty) None + else Some(word, completions) + case None => None + } } words_result match { diff -r 303123344459 -r c90cc76ec855 src/Pure/General/name_space.ML --- a/src/Pure/General/name_space.ML Tue Feb 25 19:07:42 2014 +0100 +++ b/src/Pure/General/name_space.ML Tue Feb 25 22:54:21 2014 +0100 @@ -1,8 +1,8 @@ (* Title: Pure/General/name_space.ML Author: Markus Wenzel, TU Muenchen -Generic name spaces with declared and hidden entries. Unknown names -are considered global; no support for absolute addressing. +Generic name spaces with declared and hidden entries; no support for +absolute addressing. *) type xstring = string; (*external names*) @@ -120,7 +120,7 @@ fun the_entry (Name_Space {kind, entries, ...}) name = (case Symtab.lookup entries name of - NONE => error ("Unknown " ^ kind ^ " " ^ quote name) + NONE => error (undefined kind name) | SOME (_, entry) => entry); fun entry_ord space = int_ord o pairself (#id o the_entry space); diff -r 303123344459 -r c90cc76ec855 src/Pure/Isar/args.ML --- a/src/Pure/Isar/args.ML Tue Feb 25 19:07:42 2014 +0100 +++ b/src/Pure/Isar/args.ML Tue Feb 25 22:54:21 2014 +0100 @@ -89,7 +89,7 @@ | SOME (Token.Typ T) => Syntax.pretty_typ ctxt T | SOME (Token.Term t) => Syntax.pretty_term ctxt t | SOME (Token.Fact ths) => Pretty.enclose "(" ")" (Pretty.breaks (map prt_thm ths)) - | _ => Pretty.str (Token.unparse arg)); + | _ => Pretty.mark_str (#1 (Token.markup arg), Token.unparse arg)); val (s, args) = #1 (dest_src src); in Pretty.block (Pretty.breaks (Pretty.str s :: map prt args)) end; @@ -291,8 +291,8 @@ (case Scan.error (Scan.finite' Token.stopper (Scan.option scan)) (st, args) of (SOME x, (st', [])) => (x, st') | (_, (_, args')) => - error (kind ^ " " ^ quote s ^ Position.here pos ^ ": bad arguments" ^ - (if null args' then "" else "\n " ^ space_implode " " (map Token.unparse args')))); + error ("Bad arguments for " ^ kind ^ " " ^ quote s ^ Position.here pos ^ + (if null args' then "" else ":\n " ^ space_implode " " (map Token.print args')))); fun context_syntax kind scan src = apsnd Context.the_proof o syntax kind scan src o Context.Proof; diff -r 303123344459 -r c90cc76ec855 src/Pure/Isar/attrib.ML --- a/src/Pure/Isar/attrib.ML Tue Feb 25 19:07:42 2014 +0100 +++ b/src/Pure/Isar/attrib.ML Tue Feb 25 22:54:21 2014 +0100 @@ -231,7 +231,7 @@ let val atts = map (attribute_generic context) srcs; val (th', context') = fold (uncurry o Thm.apply_attribute) atts (Drule.dummy_thm, context); - in (context', pick "" [th']) end) + in (context', pick ("", Position.none) [th']) end) || (Scan.ahead Args.alt_name -- Args.named_fact get_fact >> (fn (s, fact) => ("", Facts.Fact s, fact)) || @@ -244,7 +244,7 @@ val atts = map (attribute_generic context) srcs; val (ths', context') = fold_map (curry (fold (uncurry o Thm.apply_attribute) atts)) ths context; - in (context', pick name ths') end) + in (context', pick (name, Facts.pos_of_ref thmref) ths') end) end); in diff -r 303123344459 -r c90cc76ec855 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Tue Feb 25 19:07:42 2014 +0100 +++ b/src/Pure/Isar/isar_syn.ML Tue Feb 25 22:54:21 2014 +0100 @@ -809,7 +809,7 @@ val _ = Outer_Syntax.improper_command @{command_spec "print_methods"} "print methods of this theory" (Scan.succeed (Toplevel.unknown_theory o - Toplevel.keep (Method.print_methods o Toplevel.theory_of))); + Toplevel.keep (Method.print_methods o Toplevel.context_of))); val _ = Outer_Syntax.improper_command @{command_spec "print_antiquotations"} "print antiquotations" diff -r 303123344459 -r c90cc76ec855 src/Pure/Isar/method.ML --- a/src/Pure/Isar/method.ML Tue Feb 25 19:07:42 2014 +0100 +++ b/src/Pure/Isar/method.ML Tue Feb 25 22:54:21 2014 +0100 @@ -46,9 +46,8 @@ val raw_tactic: string * Position.T -> Proof.context -> method type src = Args.src datatype text = + Source of src | Basic of Proof.context -> method | - Source of src | - Source_i of src | Then of text list | Orelse of text list | Try of text | @@ -61,11 +60,10 @@ val done_text: text val sorry_text: bool -> text val finish_text: text option * bool -> text - val print_methods: theory -> unit - val check: theory -> xstring * Position.T -> string - val intern: theory -> xstring -> string - val method: theory -> src -> Proof.context -> method - val method_i: theory -> src -> Proof.context -> method + val print_methods: Proof.context -> unit + val the_method: Proof.context -> src -> Proof.context -> method + val check_name: Proof.context -> xstring * Position.T -> string + val check_source: Proof.context -> src -> src val syntax: 'a context_parser -> src -> Proof.context -> 'a * Proof.context val setup: binding -> (Proof.context -> method) context_parser -> string -> theory -> theory val method_setup: bstring * Position.T -> Symbol_Pos.text * Position.T -> string -> @@ -284,9 +282,8 @@ type src = Args.src; datatype text = + Source of src | Basic of Proof.context -> method | - Source of src | - Source_i of src | Then of text list | Orelse of text list | Try of text | @@ -314,10 +311,11 @@ fun merge data : T = Name_Space.merge_tables data; ); -fun print_methods thy = +val get_methods = Methods.get o Proof_Context.theory_of; + +fun print_methods ctxt = let - val ctxt = Proof_Context.init_global thy; - val meths = Methods.get thy; + val meths = get_methods ctxt; fun prt_meth (name, (_, "")) = Pretty.mark_str name | prt_meth (name, (_, comment)) = Pretty.block @@ -330,25 +328,26 @@ fun add_method name meth comment thy = thy |> Methods.map (Name_Space.define (Context.Theory thy) true (name, (meth, comment)) #> snd); - -(* get methods *) - -fun check thy = #1 o Name_Space.check (Context.Theory thy) (Methods.get thy); - -val intern = Name_Space.intern o #1 o Methods.get; - -fun method_i thy = - let - val (space, tab) = Methods.get thy; - fun meth src = +fun the_method ctxt = + let val (_, tab) = get_methods ctxt in + fn src => let val ((name, _), pos) = Args.dest_src src in (case Symtab.lookup tab name of - NONE => error ("Unknown proof method: " ^ quote name ^ Position.here pos) - | SOME (mth, _) => (Position.report pos (Name_Space.markup space name); mth src)) - end; - in meth end; + NONE => error ("Undefined method: " ^ quote name ^ Position.here pos) + | SOME (method, _) => method src) + end + end; + + +(* check *) -fun method thy = method_i thy o Args.map_name (intern thy); +fun check_name ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_methods ctxt); + +fun check_source ctxt src = + let + val ((xname, toks), pos) = Args.dest_src src; + val name = check_name ctxt (xname, pos); + in Args.src ((name, toks), pos) end; (* method setup *) @@ -406,7 +405,6 @@ fun meth4 x = (Parse.position (Parse.xname >> rpair []) >> (Source o Args.src) || - (* FIXME implicit "cartouche" method (experimental, undocumented) *) Scan.ahead Parse.cartouche |-- Parse.not_eof >> (fn tok => Source (Args.src (("cartouche", [tok]), Token.pos_of tok))) || Parse.$$$ "(" |-- Parse.!!! (meth0 --| Parse.$$$ ")")) x diff -r 303123344459 -r c90cc76ec855 src/Pure/Isar/outer_syntax.scala --- a/src/Pure/Isar/outer_syntax.scala Tue Feb 25 19:07:42 2014 +0100 +++ b/src/Pure/Isar/outer_syntax.scala Tue Feb 25 22:54:21 2014 +0100 @@ -43,7 +43,7 @@ keywords: Map[String, (String, List[String])] = Map.empty, lexicon: Scan.Lexicon = Scan.Lexicon.empty, val completion: Completion = Completion.empty, - val completion_context: Completion.Context = Completion.Context.outer, + val language_context: Completion.Language_Context = Completion.Language_Context.outer, val has_tokens: Boolean = true) { override def toString: String = @@ -73,7 +73,7 @@ val completion1 = if (Keyword.control(kind._1) || replace == Some("")) completion else completion + (name, replace getOrElse name) - new Outer_Syntax(keywords1, lexicon1, completion1, completion_context, true) + new Outer_Syntax(keywords1, lexicon1, completion1, language_context, true) } def + (name: String, kind: (String, List[String])): Outer_Syntax = @@ -151,7 +151,7 @@ /* language context */ - def set_completion_context(context: Completion.Context): Outer_Syntax = + def set_language_context(context: Completion.Language_Context): Outer_Syntax = new Outer_Syntax(keywords, lexicon, completion, context, has_tokens) def no_tokens: Outer_Syntax = @@ -159,7 +159,7 @@ require(keywords.isEmpty && lexicon.isEmpty) new Outer_Syntax( completion = completion, - completion_context = completion_context, + language_context = language_context, has_tokens = false) } } diff -r 303123344459 -r c90cc76ec855 src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Tue Feb 25 19:07:42 2014 +0100 +++ b/src/Pure/Isar/proof.ML Tue Feb 25 22:54:21 2014 +0100 @@ -392,13 +392,13 @@ Rule_Cases.make_common (Thm.theory_of_thm st, Thm.prop_of st) (map (rpair [] o rpair []) (goals st)); -fun apply_method current_context meth state = +fun apply_method current_context method state = let val (goal_ctxt, (_, {statement, messages = _, using, goal, before_qed, after_qed})) = find_goal state; val ctxt = if current_context then context_of state else goal_ctxt; in - Method.apply meth ctxt using goal |> Seq.map (fn (meth_cases, goal') => + Method.apply method ctxt using goal |> Seq.map (fn (meth_cases, goal') => state |> map_goal (Proof_Context.update_cases false (no_goal_cases goal @ goal_cases goal') #> @@ -416,13 +416,13 @@ |> Seq.lift provide_goal (PRIMITIVE (Goal.unrestrict 1) (#2 (#2 (get_goal state'))))) |> Seq.maps (apply_method true (K Method.succeed))); -fun apply_text cc text state = +fun apply_text current_context text state = let - val thy = theory_of state; + val ctxt = context_of state; - fun eval (Method.Basic m) = apply_method cc m - | eval (Method.Source src) = apply_method cc (Method.method thy src) - | eval (Method.Source_i src) = apply_method cc (Method.method_i thy src) + fun eval (Method.Basic m) = apply_method current_context m + | eval (Method.Source src) = + apply_method current_context (Method.the_method ctxt (Method.check_source ctxt src)) | eval (Method.Then txts) = Seq.EVERY (map eval txts) | eval (Method.Orelse txts) = Seq.FIRST (map eval txts) | eval (Method.Try txt) = Seq.TRY (eval txt) diff -r 303123344459 -r c90cc76ec855 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Tue Feb 25 19:07:42 2014 +0100 +++ b/src/Pure/Isar/proof_context.ML Tue Feb 25 22:54:21 2014 +0100 @@ -933,7 +933,7 @@ [res] => res | [] => err "Failed to retrieve literal fact" | _ => err "Ambiguous specification of literal fact"); - in pick "" [res] end + in pick ("", Position.none) [res] end | retrieve_thms pick ctxt xthmref = let val thy = theory_of ctxt; @@ -950,7 +950,7 @@ (Name_Space.markup (Facts.space_of local_facts) name); map (Thm.transfer thy) (Facts.select thmref ths)) | NONE => Global_Theory.get_fact (Context.Proof ctxt) thy xthmref); - in pick name thms end; + in pick (name, pos) thms end; in diff -r 303123344459 -r c90cc76ec855 src/Pure/Isar/token.ML --- a/src/Pure/Isar/token.ML Tue Feb 25 19:07:42 2014 +0100 +++ b/src/Pure/Isar/token.ML Tue Feb 25 22:54:21 2014 +0100 @@ -42,7 +42,9 @@ val inner_syntax_of: T -> string val source_position_of: T -> Symbol_Pos.text * Position.T val content_of: T -> string + val markup: T -> Markup.T * string val unparse: T -> string + val print: T -> string val text_of: T -> string * string val get_files: T -> file Exn.result list val put_files: file Exn.result list -> T -> T @@ -213,6 +215,42 @@ fun content_of (Token (_, (_, x), _)) = x; +(* markup *) + +local + +val token_kind_markup = + fn Command => (Markup.command, "") + | Keyword => (Markup.keyword2, "") + | Ident => (Markup.empty, "") + | LongIdent => (Markup.empty, "") + | SymIdent => (Markup.empty, "") + | Var => (Markup.var, "") + | TypeIdent => (Markup.tfree, "") + | TypeVar => (Markup.tvar, "") + | Nat => (Markup.empty, "") + | Float => (Markup.empty, "") + | String => (Markup.string, "") + | AltString => (Markup.altstring, "") + | Verbatim => (Markup.verbatim, "") + | Cartouche => (Markup.cartouche, "") + | Space => (Markup.empty, "") + | Comment => (Markup.comment, "") + | InternalValue => (Markup.empty, "") + | Error msg => (Markup.bad, msg) + | Sync => (Markup.control, "") + | EOF => (Markup.control, ""); + +in + +fun markup tok = + if keyword_with (not o Symbol.is_ascii_identifier) tok + then (Markup.operator, "") + else token_kind_markup (kind_of tok); + +end; + + (* unparse *) fun unparse (Token (_, (kind, x), _)) = @@ -226,16 +264,20 @@ | EOF => "" | _ => x); +fun print tok = Markup.markup (#1 (markup tok)) (unparse tok); + fun text_of tok = if is_semicolon tok then ("terminator", "") else let val k = str_of_kind (kind_of tok); + val (m, _) = markup 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 ^ " " ^ s, "") - else (k, s) + 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) end; diff -r 303123344459 -r c90cc76ec855 src/Pure/ML/ml_context.ML --- a/src/Pure/ML/ml_context.ML Tue Feb 25 19:07:42 2014 +0100 +++ b/src/Pure/ML/ml_context.ML Tue Feb 25 22:54:21 2014 +0100 @@ -25,7 +25,7 @@ val ml_store_thm: string * thm -> unit type antiq = Proof.context -> string * string val add_antiq: binding -> antiq context_parser -> theory -> theory - val check_antiq: theory -> xstring * Position.T -> string + val check_antiq: Proof.context -> xstring * Position.T -> string val trace_raw: Config.raw val trace: bool Config.T val eval_antiquotes: ML_Lex.token Antiquote.antiquote list * Position.T -> @@ -107,16 +107,17 @@ fun merge data : T = Name_Space.merge_tables data; ); +val get_antiqs = Antiq_Parsers.get o Proof_Context.theory_of; + fun add_antiq name scan thy = thy |> Antiq_Parsers.map (Name_Space.define (Context.Theory thy) true (name, scan) #> snd); -fun check_antiq thy = #1 o Name_Space.check (Context.Theory thy) (Antiq_Parsers.get thy); +fun check_antiq ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_antiqs ctxt); fun antiquotation src ctxt = let - val thy = Proof_Context.theory_of ctxt; val ((xname, _), pos) = Args.dest_src src; - val (_, scan) = Name_Space.check (Context.Proof ctxt) (Antiq_Parsers.get thy) (xname, pos); + val (_, scan) = Name_Space.check (Context.Proof ctxt) (get_antiqs ctxt) (xname, pos); in Args.context_syntax Markup.ML_antiquotationN scan src ctxt end; diff -r 303123344459 -r c90cc76ec855 src/Pure/PIDE/markup.ML --- a/src/Pure/PIDE/markup.ML Tue Feb 25 19:07:42 2014 +0100 +++ b/src/Pure/PIDE/markup.ML Tue Feb 25 22:54:21 2014 +0100 @@ -97,9 +97,8 @@ val document_antiquotation_optionN: string val paragraphN: string val paragraph: T val text_foldN: string val text_fold: T - val keywordN: string val keyword: T + val commandN: string val command: T val operatorN: string val operator: T - val commandN: string val command: T val stringN: string val string: T val altstringN: string val altstring: T val verbatimN: string val verbatim: T @@ -396,9 +395,10 @@ (* outer syntax *) -val (keywordN, keyword) = markup_elem "keyword"; +val (commandN, command) = markup_elem "command"; +val (keyword1N, keyword1) = markup_elem "keyword1"; +val (keyword2N, keyword2) = markup_elem "keyword2"; val (operatorN, operator) = markup_elem "operator"; -val (commandN, command) = markup_elem "command"; val (stringN, string) = markup_elem "string"; val (altstringN, altstring) = markup_elem "altstring"; val (verbatimN, verbatim) = markup_elem "verbatim"; @@ -409,9 +409,6 @@ val tokenN = "token"; fun token props = (tokenN, props); -val (keyword1N, keyword1) = markup_elem "keyword1"; -val (keyword2N, keyword2) = markup_elem "keyword2"; - (* timing *) diff -r 303123344459 -r c90cc76ec855 src/Pure/PIDE/markup.scala --- a/src/Pure/PIDE/markup.scala Tue Feb 25 19:07:42 2014 +0100 +++ b/src/Pure/PIDE/markup.scala Tue Feb 25 22:54:21 2014 +0100 @@ -209,9 +209,11 @@ /* outer syntax */ - val KEYWORD = "keyword" + val COMMAND = "command" + + val KEYWORD1 = "keyword1" + val KEYWORD2 = "keyword2" val OPERATOR = "operator" - val COMMAND = "command" val STRING = "string" val ALTSTRING = "altstring" val VERBATIM = "verbatim" @@ -219,9 +221,6 @@ val COMMENT = "comment" val CONTROL = "control" - val KEYWORD1 = "keyword1" - val KEYWORD2 = "keyword2" - /* timing */ diff -r 303123344459 -r c90cc76ec855 src/Pure/Thy/latex.ML --- a/src/Pure/Thy/latex.ML Tue Feb 25 19:07:42 2014 +0100 +++ b/src/Pure/Thy/latex.ML Tue Feb 25 22:54:21 2014 +0100 @@ -178,10 +178,8 @@ 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.keywordN orelse s = Markup.keyword2N - then ("\\isakeyword{", "}") + if s = Markup.commandN orelse s = Markup.keyword1N then ("\\isacommand{", "}") + else if s = Markup.keyword2N then ("\\isakeyword{", "}") else Markup.no_output; fun latex_indent "" _ = "" diff -r 303123344459 -r c90cc76ec855 src/Pure/Thy/thy_output.ML --- a/src/Pure/Thy/thy_output.ML Tue Feb 25 19:07:42 2014 +0100 +++ b/src/Pure/Thy/thy_output.ML Tue Feb 25 22:54:21 2014 +0100 @@ -14,8 +14,8 @@ val modes: string Config.T val add_wrapper: ((unit -> string) -> unit -> string) -> Proof.context -> Proof.context val add_option: binding -> (string -> Proof.context -> Proof.context) -> theory -> theory - val check_command: theory -> xstring * Position.T -> string - val check_option: theory -> xstring * Position.T -> string + val check_command: Proof.context -> xstring * Position.T -> string + val check_option: Proof.context -> xstring * Position.T -> string val print_antiquotations: Proof.context -> unit val antiquotation: binding -> 'a context_parser -> ({source: Args.src, state: Toplevel.state, context: Proof.context} -> 'a -> string) -> @@ -79,21 +79,23 @@ Name_Space.merge_tables (options1, options2)); ); +val get_antiquotations = Antiquotations.get o Proof_Context.theory_of; + fun add_command name cmd thy = thy |> Antiquotations.map (apfst (Name_Space.define (Context.Theory thy) true (name, cmd) #> snd)); fun add_option name opt thy = thy |> Antiquotations.map (apsnd (Name_Space.define (Context.Theory thy) true (name, opt) #> snd)); -fun check_command thy = #1 o Name_Space.check (Context.Theory thy) (#1 (Antiquotations.get thy)); +fun check_command ctxt = #1 o Name_Space.check (Context.Proof ctxt) (#1 (get_antiquotations ctxt)); -fun check_option thy = #1 o Name_Space.check (Context.Theory thy) (#2 (Antiquotations.get thy)); +fun check_option ctxt = #1 o Name_Space.check (Context.Proof ctxt) (#2 (get_antiquotations ctxt)); fun command src state ctxt = let - val thy = Proof_Context.theory_of ctxt; val ((xname, _), pos) = Args.dest_src src; - val (name, f) = Name_Space.check (Context.Proof ctxt) (#1 (Antiquotations.get thy)) (xname, pos); + val (name, f) = + Name_Space.check (Context.Proof ctxt) (#1 (get_antiquotations ctxt)) (xname, pos); in f src state ctxt handle ERROR msg => cat_error msg ("The error(s) above occurred in document antiquotation: " ^ @@ -102,14 +104,13 @@ fun option ((xname, pos), s) ctxt = let - val thy = Proof_Context.theory_of ctxt; - val (_, opt) = Name_Space.check (Context.Proof ctxt) (#2 (Antiquotations.get thy)) (xname, pos); + val (_, opt) = + Name_Space.check (Context.Proof ctxt) (#2 (get_antiquotations ctxt)) (xname, pos); in opt s ctxt end; fun print_antiquotations ctxt = let - val thy = Proof_Context.theory_of ctxt; - val (commands, options) = Antiquotations.get thy; + val (commands, options) = get_antiquotations ctxt; val command_names = map #1 (Name_Space.extern_table ctxt commands); val option_names = map #1 (Name_Space.extern_table ctxt options); in @@ -614,16 +615,18 @@ val _ = Theory.setup (antiquotation (Binding.name "lemma") - (Args.prop -- Scan.lift (Args.$$$ "by" |-- Method.parse -- Scan.option Method.parse)) - (fn {source, context, ...} => fn (prop, methods) => + (Args.prop -- + Scan.lift (Parse.position (Args.$$$ "by") -- (Method.parse -- Scan.option Method.parse))) + (fn {source, context = ctxt, ...} => fn (prop, ((_, by_pos), methods)) => let val prop_src = (case Args.dest_src source of ((a, arg :: _), pos) => Args.src ((a, [arg]), pos)); + val _ = Context_Position.report ctxt by_pos Markup.keyword1; (* FIXME check proof!? *) - val _ = context + val _ = ctxt |> Proof.theorem NONE (K I) [[(prop, [])]] |> Proof.global_terminal_proof methods; - in output context (maybe_pretty_source pretty_term context prop_src [prop]) end)); + in output ctxt (maybe_pretty_source pretty_term ctxt prop_src [prop]) end)); (* ML text *) diff -r 303123344459 -r c90cc76ec855 src/Pure/Thy/thy_syntax.ML --- a/src/Pure/Thy/thy_syntax.ML Tue Feb 25 19:07:42 2014 +0100 +++ b/src/Pure/Thy/thy_syntax.ML Tue Feb 25 22:54:21 2014 +0100 @@ -42,41 +42,6 @@ local -val token_kind_markup = - fn Token.Command => (Markup.command, "") - | Token.Keyword => (Markup.keyword, "") - | Token.Ident => (Markup.empty, "") - | Token.LongIdent => (Markup.empty, "") - | Token.SymIdent => (Markup.empty, "") - | Token.Var => (Markup.var, "") - | Token.TypeIdent => (Markup.tfree, "") - | Token.TypeVar => (Markup.tvar, "") - | Token.Nat => (Markup.empty, "") - | Token.Float => (Markup.empty, "") - | Token.String => (Markup.string, "") - | Token.AltString => (Markup.altstring, "") - | Token.Verbatim => (Markup.verbatim, "") - | Token.Cartouche => (Markup.cartouche, "") - | Token.Space => (Markup.empty, "") - | Token.Comment => (Markup.comment, "") - | Token.InternalValue => (Markup.empty, "") - | Token.Error msg => (Markup.bad, msg) - | Token.Sync => (Markup.control, "") - | Token.EOF => (Markup.control, ""); - -fun token_markup tok = - if Token.keyword_with (not o Symbol.is_ascii_identifier) tok - then (Markup.operator, "") - else - let - val kind = Token.kind_of tok; - val props = - if kind = Token.Command - then Markup.properties [(Markup.nameN, Token.content_of tok)] - else I; - val (markup, txt) = token_kind_markup kind; - in (props markup, txt) end; - fun reports_of_token tok = let val malformed_symbols = @@ -85,7 +50,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 (markup, txt) = token_markup tok; + val (markup, txt) = Token.markup tok; val reports = ((Token.pos_of tok, markup), txt) :: malformed_symbols; in (is_malformed, reports) end; @@ -96,7 +61,7 @@ in (exists fst results, maps snd results) end; fun present_token tok = - Markup.enclose (fst (token_markup tok)) (Output.output (Token.unparse tok)); + Markup.enclose (fst (Token.markup tok)) (Output.output (Token.unparse tok)); end; diff -r 303123344459 -r c90cc76ec855 src/Pure/facts.ML --- a/src/Pure/facts.ML Tue Feb 25 19:07:42 2014 +0100 +++ b/src/Pure/facts.ML Tue Feb 25 22:54:21 2014 +0100 @@ -6,7 +6,7 @@ signature FACTS = sig - val the_single: string -> thm list -> thm + val the_single: string * Position.T -> thm list -> thm datatype interval = FromTo of int * int | From of int | Single of int datatype ref = Named of (string * Position.T) * interval list option | @@ -46,7 +46,9 @@ (** fact references **) fun the_single _ [th] : thm = th - | the_single name _ = error ("Expected singleton fact " ^ quote name); + | the_single (name, pos) ths = + error ("Expected singleton fact " ^ quote name ^ + " (length " ^ string_of_int (length ths) ^ ")" ^ Position.here pos); (* datatype interval *) @@ -77,12 +79,15 @@ fun named name = Named ((name, Position.none), NONE); +fun name_of_ref (Named ((name, _), _)) = name + | name_of_ref (Fact _) = raise Fail "Illegal literal fact"; + +fun pos_of_ref (Named ((_, pos), _)) = pos + | pos_of_ref (Fact _) = Position.none; + fun name_pos_of_ref (Named (name_pos, _)) = name_pos | name_pos_of_ref (Fact _) = raise Fail "Illegal literal fact"; -val name_of_ref = #1 o name_pos_of_ref; -val pos_of_ref = #2 o name_pos_of_ref; - fun map_name_of_ref f (Named ((name, pos), is)) = Named ((f name, pos), is) | map_name_of_ref _ r = r; @@ -101,7 +106,7 @@ let val n = length ths; fun err msg = - error (msg ^ " for " ^ quote name ^ " (length " ^ string_of_int n ^ ")" ^ + error (msg ^ " for fact " ^ quote name ^ " (length " ^ string_of_int n ^ ")" ^ Position.here pos); fun sel i = if i < 1 orelse i > n then err ("Bad subscript " ^ string_of_int i) diff -r 303123344459 -r c90cc76ec855 src/Pure/global_theory.ML --- a/src/Pure/global_theory.ML Tue Feb 25 19:07:42 2014 +0100 +++ b/src/Pure/global_theory.ML Tue Feb 25 22:54:21 2014 +0100 @@ -86,7 +86,7 @@ end; fun get_thms thy = get_fact (Context.Theory thy) thy o Facts.named; -fun get_thm thy name = Facts.the_single name (get_thms thy name); +fun get_thm thy name = Facts.the_single (name, Position.none) (get_thms thy name); fun all_thms_of thy = Facts.fold_static (fn (_, ths) => append (map (`(Thm.get_name_hint)) ths)) (facts_of thy) []; diff -r 303123344459 -r c90cc76ec855 src/Pure/item_net.ML --- a/src/Pure/item_net.ML Tue Feb 25 19:07:42 2014 +0100 +++ b/src/Pure/item_net.ML Tue Feb 25 22:54:21 2014 +0100 @@ -54,8 +54,12 @@ mk_items eq index (x :: content) (next - 1) (fold (fn t => Net.insert_term (K false) (t, (next, x))) (index x) net); -fun merge (items1, Items {content = content2, ...}) = - fold_rev (fn y => if member items1 y then I else cons y) content2 items1; +fun merge + (items1 as Items {net = net1, ...}, + items2 as Items {net = net2, content = content2, ...}) = + if pointer_eq (net1, net2) then items1 + else if Net.is_empty net1 then items2 + else fold_rev (fn y => if member items1 y then I else cons y) content2 items1; fun remove x (items as Items {eq, index, content, next, net}) = if member items x then diff -r 303123344459 -r c90cc76ec855 src/Pure/net.ML --- a/src/Pure/net.ML Tue Feb 25 19:07:42 2014 +0100 +++ b/src/Pure/net.ML Tue Feb 25 22:54:21 2014 +0100 @@ -20,6 +20,7 @@ val encode_type: typ -> term type 'a net val empty: 'a net + val is_empty: 'a net -> bool exception INSERT val insert: ('a * 'a -> bool) -> key list * 'a -> 'a net -> 'a net val insert_term: ('a * 'a -> bool) -> term * 'a -> 'a net -> 'a net @@ -251,7 +252,8 @@ map (cons_fst VarK) (dest var) @ maps (fn (a, net) => map (cons_fst (AtomK a)) (dest net)) (Symtab.dest atoms); -fun merge eq (net1, net2) = fold (insert_safe eq) (dest net2) net1; +fun merge eq (net1, net2) = + fold (insert_safe eq) (dest net2) net1; (* FIXME non-standard merge order!?! *) fun content net = map #2 (dest net); diff -r 303123344459 -r c90cc76ec855 src/Tools/jEdit/etc/options --- a/src/Tools/jEdit/etc/options Tue Feb 25 19:07:42 2014 +0100 +++ b/src/Tools/jEdit/etc/options Tue Feb 25 22:54:21 2014 +0100 @@ -86,6 +86,7 @@ option keyword2_color : string = "009966FF" option keyword3_color : string = "0099FFFF" option caret_invisible_color : string = "50000080" +option completion_color : string = "0000FFFF" option tfree_color : string = "A020F0FF" option tvar_color : string = "A020F0FF" diff -r 303123344459 -r c90cc76ec855 src/Tools/jEdit/src/completion_popup.scala --- a/src/Tools/jEdit/src/completion_popup.scala Tue Feb 25 19:07:42 2014 +0100 +++ b/src/Tools/jEdit/src/completion_popup.scala Tue Feb 25 22:54:21 2014 +0100 @@ -92,6 +92,69 @@ } + /* rendering */ + + def rendering(rendering: Rendering, line_range: Text.Range): Option[Text.Info[Color]] = + { + active_range match { + case Some(range) => range.try_restrict(line_range) + case None => + val buffer = text_area.getBuffer + val caret = text_area.getCaretPosition + + if (line_range.contains(caret)) { + JEdit_Lib.stretch_point_range(buffer, caret).try_restrict(line_range) match { + case Some(range) if !range.is_singularity => + rendering.completion_names(range) match { + case Some(names) => Some(names.range) + case None => + syntax_completion(false, Some(rendering)) match { + case Some(result) => Some(result.range) + case None => None + } + } + case _ => None + } + } + else None + } + }.map(range => Text.Info(range, rendering.completion_color)) + + + /* syntax completion */ + + def syntax_completion( + explicit: Boolean, opt_rendering: Option[Rendering] = None): Option[Completion.Result] = + { + val buffer = text_area.getBuffer + val history = PIDE.completion_history.value + val decode = Isabelle_Encoding.is_active(buffer) + + Isabelle.mode_syntax(JEdit_Lib.buffer_mode(buffer)) match { + case Some(syntax) => + val caret = text_area.getCaretPosition + val line = buffer.getLineOfOffset(caret) + val start = buffer.getLineStartOffset(line) + val text = buffer.getSegment(start, caret - start) + + val word_context = + Completion.word_context( + JEdit_Lib.try_get_text(buffer, JEdit_Lib.point_range(buffer, caret))) + + val context = + (opt_rendering orElse PIDE.document_view(text_area).map(_.get_rendering()) match { + case Some(rendering) => + rendering.language_context(JEdit_Lib.stretch_point_range(buffer, caret)) + case None => None + }) getOrElse syntax.language_context + + syntax.completion.complete(history, decode, explicit, start, text, word_context, context) + + case None => None + } + } + + /* completion action */ private def insert(item: Completion.Item) @@ -156,64 +219,37 @@ } } - def semantic_completion(): Boolean = - explicit && { + def semantic_completion(): Option[Completion.Result] = + if (explicit) { PIDE.document_view(text_area) match { case Some(doc_view) => val rendering = doc_view.get_rendering() rendering.completion_names(JEdit_Lib.stretch_point_range(buffer, caret)) match { - case None => false + case None => None case Some(names) => JEdit_Lib.try_get_text(buffer, names.range) match { - case Some(original) => - names.complete(history, decode, original) match { - case Some(result) if !result.items.isEmpty => - open_popup(result) - true - case _ => false - } - case None => false + case Some(original) => names.complete(history, decode, original) + case None => None } } - case _ => false + case None => None } } - - def syntax_completion(): Boolean = - { - Isabelle.mode_syntax(JEdit_Lib.buffer_mode(buffer)) match { - case Some(syntax) => - val line = buffer.getLineOfOffset(caret) - val start = buffer.getLineStartOffset(line) - val text = buffer.getSegment(start, caret - start) + else None - val context = - (PIDE.document_view(text_area) match { - case None => None - case Some(doc_view) => - val rendering = doc_view.get_rendering() - rendering.completion_context(JEdit_Lib.stretch_point_range(buffer, caret)) - }) getOrElse syntax.completion_context - - syntax.completion.complete(history, decode, explicit, start, text, context) match { - case Some(result) => - result.items match { - case List(item) if result.unique && item.immediate && immediate => - insert(item) - true - case _ :: _ => - open_popup(result) - true - case _ => false - } - case None => false + if (buffer.isEditable) { + semantic_completion() orElse syntax_completion(explicit) match { + case Some(result) => + result.items match { + case List(item) if result.unique && item.immediate && immediate => + insert(item) + case _ :: _ => + open_popup(result) + case _ => } - case None => false + case None => } } - - if (buffer.isEditable) - semantic_completion() || syntax_completion() } @@ -346,8 +382,13 @@ val caret = text_field.getCaret.getDot val text = text_field.getText.substring(0, caret) - syntax.completion.complete( - history, decode = true, explicit = false, 0, text, syntax.completion_context) match { + val word_context = + Completion.word_context(JEdit_Lib.try_get_text(text_field.getText, + Text.Range(caret, caret + 1))) // FIXME proper point range!? + + val context = syntax.language_context + + syntax.completion.complete(history, true, false, 0, text, word_context, context) match { case Some(result) => val fm = text_field.getFontMetrics(text_field.getFont) val loc = diff -r 303123344459 -r c90cc76ec855 src/Tools/jEdit/src/isabelle.scala --- a/src/Tools/jEdit/src/isabelle.scala Tue Feb 25 19:07:42 2014 +0100 +++ b/src/Tools/jEdit/src/isabelle.scala Tue Feb 25 22:54:21 2014 +0100 @@ -33,7 +33,7 @@ private lazy val ml_syntax: Outer_Syntax = Outer_Syntax.init().no_tokens. - set_completion_context(Completion.Context.ML_outer) + set_language_context(Completion.Language_Context.ML_outer) private lazy val news_syntax: Outer_Syntax = Outer_Syntax.init().no_tokens diff -r 303123344459 -r c90cc76ec855 src/Tools/jEdit/src/rendering.scala --- a/src/Tools/jEdit/src/rendering.scala Tue Feb 25 19:07:42 2014 +0100 +++ b/src/Tools/jEdit/src/rendering.scala Tue Feb 25 22:54:21 2014 +0100 @@ -152,7 +152,7 @@ private val completion_names_elements = Set(Markup.COMPLETION) - private val completion_context_elements = + private val language_context_elements = Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM, Markup.CARTOUCHE, Markup.COMMENT, Markup.LANGUAGE, Markup.ML_STRING, Markup.ML_COMMENT) @@ -261,6 +261,7 @@ val keyword2_color = color_value("keyword2_color") val keyword3_color = color_value("keyword3_color") val caret_invisible_color = color_value("caret_invisible_color") + val completion_color = color_value("completion_color") val tfree_color = color_value("tfree_color") val tvar_color = color_value("tvar_color") @@ -287,16 +288,16 @@ }).headOption.map(_.info) } - def completion_context(range: Text.Range): Option[Completion.Context] = - snapshot.select(range, Rendering.completion_context_elements, _ => + def language_context(range: Text.Range): Option[Completion.Language_Context] = + snapshot.select(range, Rendering.language_context_elements, _ => { + case Text.Info(_, XML.Elem(Markup.Language(language, symbols, antiquotes), _)) => + Some(Completion.Language_Context(language, symbols, antiquotes)) case Text.Info(_, elem) if elem.name == Markup.ML_STRING || elem.name == Markup.ML_COMMENT => - Some(Completion.Context.ML_inner) - case Text.Info(_, XML.Elem(Markup.Language(language, symbols, antiquotes), _)) => - Some(Completion.Context(language, symbols, antiquotes)) + Some(Completion.Language_Context.ML_inner) case Text.Info(_, _) => - Some(Completion.Context.inner) + Some(Completion.Language_Context.inner) }).headOption.map(_.info) diff -r 303123344459 -r c90cc76ec855 src/Tools/jEdit/src/rich_text_area.scala --- a/src/Tools/jEdit/src/rich_text_area.scala Tue Feb 25 19:07:42 2014 +0100 +++ b/src/Tools/jEdit/src/rich_text_area.scala Tue Feb 25 22:54:21 2014 +0100 @@ -222,23 +222,6 @@ } - /* caret */ - - private def get_caret_range(stretch: Boolean): Text.Range = - if (caret_visible) { - val caret = text_area.getCaretPosition - if (stretch) JEdit_Lib.stretch_point_range(buffer, caret) - else JEdit_Lib.point_range(buffer, caret) - } - else Text.Range(-1) - - private def get_caret_color(rendering: Rendering): Color = - { - if (text_area.isCaretVisible) text_area.getPainter.getCaretColor - else rendering.caret_invisible_color - } - - /* text background */ private val background_painter = new TextAreaExtension @@ -312,13 +295,23 @@ /* text */ + private def caret_color(rendering: Rendering): Color = + { + if (text_area.isCaretVisible) + text_area.getPainter.getCaretColor + else rendering.caret_invisible_color + } + private def paint_chunk_list(rendering: Rendering, gfx: Graphics2D, line_start: Text.Offset, head: Chunk, x: Float, y: Float): Float = { val clip_rect = gfx.getClipBounds val painter = text_area.getPainter val font_context = painter.getFontRenderContext - val caret_range = get_caret_range(false) + + val caret_range = + if (caret_visible) JEdit_Lib.point_range(buffer, text_area.getCaretPosition) + else Text.Range(-1) var w = 0.0f var chunk = head @@ -369,7 +362,7 @@ val astr = new AttributedString(s2) astr.addAttribute(TextAttribute.FONT, chunk_font) - astr.addAttribute(TextAttribute.FOREGROUND, get_caret_color(rendering)) + astr.addAttribute(TextAttribute.FOREGROUND, caret_color(rendering)) astr.addAttribute(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON) gfx.drawString(astr.getIterator, x1 + string_width(s1), y) @@ -455,9 +448,6 @@ start: Array[Int], end: Array[Int], y: Int, line_height: Int) { robust_rendering { rendering => - val caret_range = get_caret_range(true) - val caret_color = text_area.getPainter.getCaretColor - for (i <- 0 until physical_lines.length) { if (physical_lines(i) != -1) { val line_range = Text.Range(start(i), end(i)) @@ -492,21 +482,14 @@ } // completion range - if (!hyperlink_area.is_active) { - def paint_completion(range: Text.Range) { - for (r <- JEdit_Lib.gfx_range(text_area, range)) { - gfx.setColor(caret_color) - gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1) - } - } - Completion_Popup.Text_Area.active_range(text_area) match { - case Some(range) if range.try_restrict(line_range).isDefined => - paint_completion(range.try_restrict(line_range).get) - case _ => - for { - caret <- caret_range.try_restrict(line_range) - names <- rendering.completion_names(caret) - } paint_completion(names.range) + if (!hyperlink_area.is_active && caret_visible) { + for { + completion <- Completion_Popup.Text_Area(text_area) + Text.Info(range, color) <- completion.rendering(rendering, line_range) + r <- JEdit_Lib.gfx_range(text_area, range) + } { + gfx.setColor(color) + gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1) } } } @@ -550,7 +533,7 @@ val offset = caret - text_area.getLineStartOffset(physical_line) val x = text_area.offsetToXY(physical_line, offset).x - gfx.setColor(get_caret_color(rendering)) + gfx.setColor(caret_color(rendering)) gfx.drawRect(x, y, (metric.unit * metric.average).round.toInt - 1, fm.getHeight - 1) } } diff -r 303123344459 -r c90cc76ec855 src/ZF/Tools/induct_tacs.ML --- a/src/ZF/Tools/induct_tacs.ML Tue Feb 25 19:07:42 2014 +0100 +++ b/src/ZF/Tools/induct_tacs.ML Tue Feb 25 22:54:21 2014 +0100 @@ -166,8 +166,8 @@ fun rep_datatype raw_elim raw_induct raw_case_eqns raw_recursor_eqns thy = let val ctxt = Proof_Context.init_global thy; - val elim = Facts.the_single "elimination" (Attrib.eval_thms ctxt [raw_elim]); - val induct = Facts.the_single "induction" (Attrib.eval_thms ctxt [raw_induct]); + val elim = Facts.the_single ("elimination", Position.none) (Attrib.eval_thms ctxt [raw_elim]); + val induct = Facts.the_single ("induction", Position.none) (Attrib.eval_thms ctxt [raw_induct]); val case_eqns = Attrib.eval_thms ctxt raw_case_eqns; val recursor_eqns = Attrib.eval_thms ctxt raw_recursor_eqns; in rep_datatype_i elim induct case_eqns recursor_eqns thy end;