--- 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;
--- 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:
+ "\<forall>x.
+ \<not> P {fst x..snd x} \<longrightarrow>
+ \<not> P {fst (f x)..snd (f x)} \<and>
+ (\<forall>i\<in>Basis.
+ fst x \<bullet> i \<le> fst (f x) \<bullet> i \<and>
+ fst (f x) \<bullet> i \<le> snd (f x) \<bullet> i \<and>
+ snd (f x) \<bullet> i \<le> snd x \<bullet> i \<and>
+ 2 * (snd (f x) \<bullet> i - fst (f x) \<bullet> i) \<le> snd x \<bullet> i - fst x \<bullet> i)"
apply -
apply (drule choice)
- apply (erule exE)
- done
- note f = this
+ apply blast
+ done
def AB \<equiv> "\<lambda>n. (f ^^ n) (a,b)"
def A \<equiv> "\<lambda>n. fst(AB n)"
def B \<equiv> "\<lambda>n. snd(AB n)"
@@ -2300,7 +2307,14 @@
then show thesis ..
next
assume as: "\<not> (\<exists>p. p tagged_division_of {a..b} \<and> g fine p)"
- guess x
+ obtain x where x:
+ "x \<in> {a..b}"
+ "\<And>e. 0 < e \<Longrightarrow>
+ \<exists>c d.
+ x \<in> {c..d} \<and>
+ {c..d} \<subseteq> ball x e \<and>
+ {c..d} \<subseteq> {a..b} \<and>
+ \<not> (\<exists>p. p tagged_division_of {c..d} \<and> g fine p)"
apply (rule interval_bisection[of "\<lambda>s. \<exists>p. p tagged_division_of s \<and> 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 \<subseteq> 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"
+ "\<And>p. p tagged_division_of {a..b} \<Longrightarrow>
+ d1 fine p \<Longrightarrow> norm ((\<Sum>(x, k)\<in>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"
+ "\<And>p. p tagged_division_of {a..b} \<Longrightarrow>
+ d2 fine p \<Longrightarrow> norm ((\<Sum>(x, k)\<in>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}"
+ "(\<lambda>x. d1 x \<inter> d2 x) fine p"
+ by (rule fine_division_exists[OF gauge_inter[OF d1(1) d2(1)]])
let ?c = "(\<Sum>(x, k)\<in>p. content k *\<^sub>R f x)"
have "norm (k1 - k2) \<le> norm (?c - k2) + norm (?c - k1)"
using norm_triangle_ineq4[of "k1 - ?c" "k2 - ?c"]
@@ -2379,8 +2404,18 @@
done
}
assume as: "\<not> (\<exists>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"
+ "\<And>a b. ball 0 B1 \<subseteq> {a..b} \<Longrightarrow>
+ \<exists>z. ((\<lambda>x. if x \<in> i then f x else 0) has_integral z) {a..b} \<and>
+ 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"
+ "\<And>a b. ball 0 B2 \<subseteq> {a..b} \<Longrightarrow>
+ \<exists>z. ((\<lambda>x. if x \<in> i then f x else 0) has_integral z) {a..b} \<and>
+ norm (z - k2) < norm (k1 - k2) / 2"
+ by (rule has_integral_altD[OF assms(2) as,OF e]) blast
have "\<exists>a b::'n. ball 0 B1 \<union> ball 0 B2 \<subseteq> {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"
+ "\<And>a b. ball 0 B1 \<subseteq> {a..b} \<Longrightarrow>
+ \<exists>z. ((\<lambda>x. if x \<in> s then f x else 0) has_integral z) {a..b} \<and> norm (z - k) < e / 2"
+ by blast
+ from has_integral_altD[OF assms(2) as *]
+ obtain B2 where B2:
+ "0 < B2"
+ "\<And>a b. ball 0 B2 \<subseteq> {a..b} \<Longrightarrow>
+ \<exists>z. ((\<lambda>x. if x \<in> s then g x else 0) has_integral z) {a..b} \<and> norm (z - l) < e / 2"
+ by blast
show ?case
apply (rule_tac x="max B1 B2" in exI)
apply rule
--- 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;
--- 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 {
--- 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);
--- 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;
--- 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
--- 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"
--- 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
--- 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)
}
}
--- 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)
--- 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
--- 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;
--- 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;
--- 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 *)
--- 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 */
--- 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 "" _ = ""
--- 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 *)
--- 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;
--- 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)
--- 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) [];
--- 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
--- 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);
--- 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"
--- 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 =
--- 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
--- 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)
--- 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)
}
}
--- 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;