--- a/src/HOL/Bali/DeclConcepts.thy Sat Nov 12 13:01:56 2011 +0100
+++ b/src/HOL/Bali/DeclConcepts.thy Sat Nov 12 20:14:09 2011 +0100
@@ -1071,25 +1071,16 @@
done
lemma member_of_Package:
- "\<lbrakk>G\<turnstile>m member_of C; accmodi m = Package\<rbrakk>
- \<Longrightarrow> pid (declclass m) = pid C"
-proof -
- assume member: "G\<turnstile>m member_of C"
- then show " accmodi m = Package \<Longrightarrow> ?thesis" (is "PROP ?P m C")
- proof (induct rule: members.induct)
- fix C m
- assume C: "declclass m = C"
- then show "pid (declclass m) = pid C"
- by simp
- next
- fix C S m
- assume inheritable: "G \<turnstile> m inheritable_in pid C"
- assume hyp: "PROP ?P m S" and
- package_acc: "accmodi m = Package"
- with inheritable package_acc hyp
- show "pid (declclass m) = pid C"
- by (auto simp add: inheritable_in_def)
- qed
+ assumes "G\<turnstile>m member_of C"
+ and "accmodi m = Package"
+ shows "pid (declclass m) = pid C"
+ using assms
+proof induct
+ case Immediate
+ then show ?case by simp
+next
+ case Inherited
+ then show ?case by (auto simp add: inheritable_in_def)
qed
lemma member_in_declC: "G\<turnstile>m member_in C\<Longrightarrow> G\<turnstile>m member_in (declclass m)"
@@ -1581,19 +1572,14 @@
apply (force elim: imethds_norec intro: rtrancl_into_rtrancl2)
done
-lemma imethds_cases [consumes 3, case_names NewMethod InheritedMethod]:
- assumes im: "im \<in> imethds G I sig" and
- ifI: "iface G I = Some i" and
- ws: "ws_prog G" and
- hyp_new: "table_of (map (\<lambda>(s, mh). (s, I, mh)) (imethods i)) sig
- = Some im \<Longrightarrow> P" and
- hyp_inh: "\<And> J. \<lbrakk>J \<in> set (isuperIfs i); im \<in> imethds G J sig\<rbrakk> \<Longrightarrow> P"
- shows P
-proof -
- from ifI ws im hyp_new hyp_inh
- show "P"
- by (auto simp add: imethds_rec)
-qed
+lemma imethds_cases:
+ assumes im: "im \<in> imethds G I sig"
+ and ifI: "iface G I = Some i"
+ and ws: "ws_prog G"
+ obtains (NewMethod) "table_of (map (\<lambda>(s, mh). (s, I, mh)) (imethods i)) sig = Some im"
+ | (InheritedMethod) J where "J \<in> set (isuperIfs i)" and "im \<in> imethds G J sig"
+using assms by (auto simp add: imethds_rec)
+
subsection "accimethd"
@@ -1758,7 +1744,7 @@
lemma accmethd_SomeD:
"accmethd G S C sig = Some m
\<Longrightarrow> methd G C sig = Some m \<and> G\<turnstile>method sig m of C accessible_from S"
-by (auto simp add: accmethd_def dest: filter_tab_SomeD)
+by (auto simp add: accmethd_def)
lemma accmethd_SomeI:
"\<lbrakk>methd G C sig = Some m; G\<turnstile>method sig m of C accessible_from S\<rbrakk>
@@ -1836,13 +1822,13 @@
next
case (Some statM)
note statM = Some
- let "?filter C" =
- "filter_tab
+ let ?filter =
+ "\<lambda>C. filter_tab
(\<lambda>_ dynM. G,sig \<turnstile> dynM overrides statM \<or> dynM = statM)
(methd G C)"
- let "?class_rec C" =
- "(class_rec G C empty
- (\<lambda>C c subcls_mthds. subcls_mthds ++ (?filter C)))"
+ let ?class_rec =
+ "\<lambda>C. class_rec G C empty
+ (\<lambda>C c subcls_mthds. subcls_mthds ++ (?filter C))"
from statM Subcls ws subclseq_dynC_statC
have dynmethd_dynC_def:
"?Dynmethd_def dynC sig =
@@ -1924,18 +1910,19 @@
\<Longrightarrow> G\<turnstile>dynC \<preceq>\<^sub>C statC \<and> (\<exists> statM. methd G statC sig = Some statM)"
by (auto simp add: dynmethd_rec)
-lemma dynmethd_Some_cases [consumes 3, case_names Static Overrides]:
- assumes dynM: "dynmethd G statC dynC sig = Some dynM" and
- is_cls_dynC: "is_class G dynC" and
- ws: "ws_prog G" and
- hyp_static: "methd G statC sig = Some dynM \<Longrightarrow> P" and
- hyp_override: "\<And> statM. \<lbrakk>methd G statC sig = Some statM;dynM\<noteq>statM;
- G,sig\<turnstile>dynM overrides statM\<rbrakk> \<Longrightarrow> P"
- shows P
+lemma dynmethd_Some_cases:
+ assumes dynM: "dynmethd G statC dynC sig = Some dynM"
+ and is_cls_dynC: "is_class G dynC"
+ and ws: "ws_prog G"
+ obtains (Static) "methd G statC sig = Some dynM"
+ | (Overrides) statM
+ where "methd G statC sig = Some statM"
+ and "dynM \<noteq> statM"
+ and "G,sig\<turnstile>dynM overrides statM"
proof -
from is_cls_dynC obtain dc where clsDynC: "class G dynC = Some dc" by blast
- from clsDynC ws dynM hyp_static hyp_override
- show "P"
+ from clsDynC ws dynM Static Overrides
+ show ?thesis
proof (induct rule: ws_class_induct)
case (Object co)
with ws have "statC = Object"
@@ -1972,25 +1959,20 @@
qed
-lemma dynmethd_Some_rec_cases [consumes 3,
- case_names Static Override Recursion]:
- assumes dynM: "dynmethd G statC dynC sig = Some dynM" and
- clsDynC: "class G dynC = Some c" and
- ws: "ws_prog G" and
- hyp_static: "methd G statC sig = Some dynM \<Longrightarrow> P" and
- hyp_override: "\<And> statM. \<lbrakk>methd G statC sig = Some statM;
- methd G dynC sig = Some dynM; statM\<noteq>dynM;
- G,sig\<turnstile> dynM overrides statM\<rbrakk> \<Longrightarrow> P" and
-
- hyp_recursion: "\<lbrakk>dynC\<noteq>Object;
- dynmethd G statC (super c) sig = Some dynM\<rbrakk> \<Longrightarrow> P"
- shows P
+lemma dynmethd_Some_rec_cases:
+ assumes dynM: "dynmethd G statC dynC sig = Some dynM"
+ and clsDynC: "class G dynC = Some c"
+ and ws: "ws_prog G"
+ obtains (Static) "methd G statC sig = Some dynM"
+ | (Override) statM where "methd G statC sig = Some statM"
+ and "methd G dynC sig = Some dynM" and "statM \<noteq> dynM"
+ and "G,sig\<turnstile> dynM overrides statM"
+ | (Recursion) "dynC \<noteq> Object" and "dynmethd G statC (super c) sig = Some dynM"
proof -
- from clsDynC have "is_class G dynC" by simp
- note no_override_in_Object' = no_override_in_Object [OF dynM this ws]
- from ws clsDynC dynM hyp_static hyp_override hyp_recursion
+ from clsDynC have *: "is_class G dynC" by simp
+ from ws clsDynC dynM Static Override Recursion
show ?thesis
- by (auto simp add: dynmethd_rec dest: no_override_in_Object')
+ by (auto simp add: dynmethd_rec dest: no_override_in_Object [OF dynM * ws])
qed
lemma dynmethd_declC:
@@ -2095,24 +2077,22 @@
qed
qed
-lemma dynmethd_cases [consumes 4, case_names Static Overrides]:
- assumes statM: "methd G statC sig = Some statM" and
- subclseq: "G\<turnstile>dynC \<preceq>\<^sub>C statC" and
- is_cls_statC: "is_class G statC" and
- ws: "ws_prog G" and
- hyp_static: "dynmethd G statC dynC sig = Some statM \<Longrightarrow> P" and
- hyp_override: "\<And> dynM. \<lbrakk>dynmethd G statC dynC sig = Some dynM;
- dynM\<noteq>statM;
- G,sig\<turnstile>dynM overrides statM\<rbrakk> \<Longrightarrow> P"
- shows P
+lemma dynmethd_cases:
+ assumes statM: "methd G statC sig = Some statM"
+ and subclseq: "G\<turnstile>dynC \<preceq>\<^sub>C statC"
+ and is_cls_statC: "is_class G statC"
+ and ws: "ws_prog G"
+ obtains (Static) "dynmethd G statC dynC sig = Some statM"
+ | (Overrides) dynM where "dynmethd G statC dynC sig = Some dynM"
+ and "dynM \<noteq> statM" and "G,sig\<turnstile>dynM overrides statM"
proof -
+ note hyp_static = Static and hyp_override = Overrides
from subclseq is_cls_statC
have is_cls_dynC: "is_class G dynC" by (rule subcls_is_class2)
then obtain dc where
clsDynC: "class G dynC = Some dc" by blast
from statM subclseq is_cls_statC ws
- obtain dynM
- where dynM: "dynmethd G statC dynC sig = Some dynM"
+ obtain dynM where dynM: "dynmethd G statC dynC sig = Some dynM"
by (blast dest: methd_Some_dynmethd_Some)
from dynM is_cls_dynC ws
show ?thesis
@@ -2151,14 +2131,13 @@
subsection "dynlookup"
-lemma dynlookup_cases [consumes 1, case_names NullT IfaceT ClassT ArrayT]:
-"\<lbrakk>dynlookup G statT dynC sig = x;
- \<lbrakk>statT = NullT ; empty sig = x \<rbrakk> \<Longrightarrow> P;
- \<And> I. \<lbrakk>statT = IfaceT I ; dynimethd G I dynC sig = x\<rbrakk> \<Longrightarrow> P;
- \<And> statC.\<lbrakk>statT = ClassT statC; dynmethd G statC dynC sig = x\<rbrakk> \<Longrightarrow> P;
- \<And> ty. \<lbrakk>statT = ArrayT ty ; dynmethd G Object dynC sig = x\<rbrakk> \<Longrightarrow> P
- \<rbrakk> \<Longrightarrow> P"
-by (cases statT) (auto simp add: dynlookup_def)
+lemma dynlookup_cases:
+ assumes "dynlookup G statT dynC sig = x"
+ obtains (NullT) "statT = NullT" and "empty sig = x"
+ | (IfaceT) I where "statT = IfaceT I" and "dynimethd G I dynC sig = x"
+ | (ClassT) statC where "statT = ClassT statC" and "dynmethd G statC dynC sig = x"
+ | (ArrayT) ty where "statT = ArrayT ty" and "dynmethd G Object dynC sig = x"
+using assms by (cases statT) (auto simp add: dynlookup_def)
subsection "fields"
--- a/src/Pure/PIDE/document.scala Sat Nov 12 13:01:56 2011 +0100
+++ b/src/Pure/PIDE/document.scala Sat Nov 12 20:14:09 2011 +0100
@@ -240,9 +240,8 @@
def convert(range: Text.Range): Text.Range
def revert(i: Text.Offset): Text.Offset
def revert(range: Text.Range): Text.Range
- def cumulate_markup[A](info: Text.Info[A])(result: Markup_Tree.Cumulate[A])
- : Stream[Text.Info[A]]
- def select_markup[A](range: Text.Range)(result: Markup_Tree.Select[A])
+ def cumulate_markup[A](range: Text.Range)(body: Markup_Tree.Cumulate[A]): Stream[Text.Info[A]]
+ def select_markup[A](range: Text.Range)(body: Markup_Tree.Select[A])
: Stream[Text.Info[Option[A]]]
}
@@ -473,34 +472,37 @@
def convert(range: Text.Range) = (range /: edits)((r, edit) => edit.convert(r))
def revert(range: Text.Range) = (range /: reverse_edits)((r, edit) => edit.revert(r))
- def cumulate_markup[A](root: Text.Info[A])(result: Markup_Tree.Cumulate[A])
+ def cumulate_markup[A](range: Text.Range)(body: Markup_Tree.Cumulate[A])
: Stream[Text.Info[A]] =
{
- val former_range = revert(root.range)
+ val info = body.info
+ val result = body.result
+
+ val former_range = revert(range)
for {
(command, command_start) <- node.command_range(former_range).toStream
Text.Info(r0, a) <- command_state(command).markup.
- cumulate(Text.Info((former_range - command_start).restrict(command.range), root.info)) {
- case (a, Text.Info(r0, b))
- if result.isDefinedAt((a, Text.Info(convert(r0 + command_start), b))) =>
- result((a, Text.Info(convert(r0 + command_start), b)))
- }
+ cumulate((former_range - command_start).restrict(command.range))(
+ Markup_Tree.Cumulate[A](info,
+ {
+ case (a, Text.Info(r0, b))
+ if result.isDefinedAt((a, Text.Info(convert(r0 + command_start), b))) =>
+ result((a, Text.Info(convert(r0 + command_start), b)))
+ },
+ body.elements))
} yield Text.Info(convert(r0 + command_start), a)
}
- def select_markup[A](range: Text.Range)(result: Markup_Tree.Select[A])
+ def select_markup[A](range: Text.Range)(body: Markup_Tree.Select[A])
: Stream[Text.Info[Option[A]]] =
{
- val former_range = revert(range)
- for {
- (command, command_start) <- node.command_range(former_range).toStream
- Text.Info(r0, x) <- command_state(command).markup.
- select((former_range - command_start).restrict(command.range)) {
- case Text.Info(r0, info)
- if result.isDefinedAt(Text.Info(convert(r0 + command_start), info)) =>
- result(Text.Info(convert(r0 + command_start), info))
- }
- } yield Text.Info(convert(r0 + command_start), x)
+ val result = body.result
+ val result1 =
+ new PartialFunction[(Option[A], Text.Markup), Option[A]] {
+ def isDefinedAt(arg: (Option[A], Text.Markup)): Boolean = result.isDefinedAt(arg._2)
+ def apply(arg: (Option[A], Text.Markup)): Option[A] = Some(result(arg._2))
+ }
+ cumulate_markup(range)(Markup_Tree.Cumulate[Option[A]](None, result1, body.elements))
}
}
}
--- a/src/Pure/PIDE/markup_tree.scala Sat Nov 12 13:01:56 2011 +0100
+++ b/src/Pure/PIDE/markup_tree.scala Sat Nov 12 20:14:09 2011 +0100
@@ -15,25 +15,46 @@
object Markup_Tree
{
- type Cumulate[A] = PartialFunction[(A, Text.Markup), A]
- type Select[A] = PartialFunction[Text.Markup, A]
+ sealed case class Cumulate[A](
+ info: A, result: PartialFunction[(A, Text.Markup), A], elements: Option[Set[String]])
+ sealed case class Select[A](
+ result: PartialFunction[Text.Markup, A], elements: Option[Set[String]])
val empty: Markup_Tree = new Markup_Tree(Branches.empty)
+ object Entry
+ {
+ def apply(markup: Text.Markup, subtree: Markup_Tree): Entry =
+ Entry(markup.range, List(markup.info), Set(markup.info.markup.name), subtree)
+ }
+
+ sealed case class Entry(
+ range: Text.Range,
+ rev_markup: List[XML.Elem],
+ elements: Set[String],
+ subtree: Markup_Tree)
+ {
+ def + (info: XML.Elem): Entry =
+ if (elements(info.markup.name)) copy(rev_markup = info :: rev_markup)
+ else copy(rev_markup = info :: rev_markup, elements = elements + info.markup.name)
+
+ def markup: List[XML.Elem] = rev_markup.reverse
+ }
+
object Branches
{
- type Entry = (Text.Markup, Markup_Tree)
type T = SortedMap[Text.Range, Entry]
-
val empty: T = SortedMap.empty(Text.Range.Ordering)
- def update(branches: T, entry: Entry): T = branches + (entry._1.range -> entry)
- def single(entry: Entry): T = update(empty, entry)
}
}
class Markup_Tree private(branches: Markup_Tree.Branches.T)
{
+ private def this(branches: Markup_Tree.Branches.T, entry: Markup_Tree.Entry) =
+ this(branches + (entry.range -> entry))
+
+
import Markup_Tree._
override def toString =
@@ -42,104 +63,85 @@
case list => list.mkString("Tree(", ",", ")")
}
- private def overlapping(range: Text.Range): Branches.T = // FIXME special cases!?
+ private def overlapping(range: Text.Range): Branches.T =
{
val start = Text.Range(range.start)
val stop = Text.Range(range.stop)
val bs = branches.range(start, stop)
// FIXME check after Scala 2.8.x
branches.get(stop) match {
- case Some(end) if range overlaps end._1.range => Branches.update(bs, end)
+ case Some(end) if range overlaps end.range => bs + (end.range -> end)
case _ => bs
}
}
- def + (new_info: Text.Markup): Markup_Tree =
+ def + (new_markup: Text.Markup): Markup_Tree =
{
- val new_range = new_info.range
+ val new_range = new_markup.range
+
branches.get(new_range) match {
- case None =>
- new Markup_Tree(Branches.update(branches, new_info -> empty))
- case Some((info, subtree)) =>
- val range = info.range
- if (range.contains(new_range))
- new Markup_Tree(Branches.update(branches, info -> (subtree + new_info)))
+ case None => new Markup_Tree(branches, Entry(new_markup, empty))
+ case Some(entry) =>
+ if (entry.range == new_range)
+ new Markup_Tree(branches, entry + new_markup.info)
+ else if (entry.range.contains(new_range))
+ new Markup_Tree(branches, entry.copy(subtree = entry.subtree + new_markup))
else if (new_range.contains(branches.head._1) && new_range.contains(branches.last._1))
- new Markup_Tree(Branches.single(new_info -> this))
+ new Markup_Tree(Branches.empty, Entry(new_markup, this))
else {
val body = overlapping(new_range)
if (body.forall(e => new_range.contains(e._1))) {
- val rest = // branches -- body, modulo workarounds for Redblack in Scala 2.8.0
+ val rest = // branches -- body, modulo workarounds for Redblack in Scala 2.8.0 FIXME
if (body.size > 1)
(Branches.empty /: branches)((rest, entry) =>
if (body.isDefinedAt(entry._1)) rest else rest + entry)
else branches
- new Markup_Tree(Branches.update(rest, new_info -> new Markup_Tree(body)))
+ new Markup_Tree(rest, Entry(new_markup, new Markup_Tree(body)))
}
else { // FIXME split markup!?
- System.err.println("Ignored overlapping markup information: " + new_info)
+ System.err.println("Ignored overlapping markup information: " + new_markup)
this
}
}
}
}
- def cumulate[A](root: Text.Info[A])(result: Cumulate[A]): Stream[Text.Info[A]] =
+ def cumulate[A](root_range: Text.Range)(body: Cumulate[A]): Stream[Text.Info[A]] =
{
+ val root_info = body.info
+
+ def result(x: A, entry: Entry): Option[A] =
+ if (body.elements match { case Some(es) => es.exists(entry.elements) case None => true }) {
+ val (y, changed) =
+ (entry.markup :\ (x, false))((info, res) =>
+ {
+ val (y, changed) = res
+ val arg = (x, Text.Info(entry.range, info))
+ if (body.result.isDefinedAt(arg)) (body.result(arg), true)
+ else res
+ })
+ if (changed) Some(y) else None
+ }
+ else None
+
def stream(
last: Text.Offset,
- stack: List[(Text.Info[A], Stream[(Text.Range, Branches.Entry)])]): Stream[Text.Info[A]] =
+ stack: List[(Text.Info[A], Stream[(Text.Range, Entry)])]): Stream[Text.Info[A]] =
{
stack match {
- case (parent, (range, (info, tree)) #:: more) :: rest =>
- val subrange = range.restrict(root.range)
- val subtree = tree.overlapping(subrange).toStream
+ case (parent, (range, entry) #:: more) :: rest =>
+ val subrange = range.restrict(root_range)
+ val subtree = entry.subtree.overlapping(subrange).toStream
val start = subrange.start
- val arg = (parent.info, info)
- if (result.isDefinedAt(arg)) {
- val next = Text.Info(subrange, result(arg))
- val nexts = stream(start, (next, subtree) :: (parent, more) :: rest)
- if (last < start) parent.restrict(Text.Range(last, start)) #:: nexts
- else nexts
+ result(parent.info, entry) match {
+ case Some(res) =>
+ val next = Text.Info(subrange, res)
+ val nexts = stream(start, (next, subtree) :: (parent, more) :: rest)
+ if (last < start) parent.restrict(Text.Range(last, start)) #:: nexts
+ else nexts
+ case None => stream(last, (parent, subtree #::: more) :: rest)
}
- else stream(last, (parent, subtree #::: more) :: rest)
-
- case (parent, Stream.Empty) :: rest =>
- val stop = parent.range.stop
- val nexts = stream(stop, rest)
- if (last < stop) parent.restrict(Text.Range(last, stop)) #:: nexts
- else nexts
-
- case Nil =>
- val stop = root.range.stop
- if (last < stop) Stream(root.restrict(Text.Range(last, stop)))
- else Stream.empty
- }
- }
- stream(root.range.start, List((root, overlapping(root.range).toStream)))
- }
-
- def select[A](root_range: Text.Range)(result: Select[A]): Stream[Text.Info[Option[A]]] =
- {
- def stream(
- last: Text.Offset,
- stack: List[(Text.Info[Option[A]], Stream[(Text.Range, Branches.Entry)])])
- : Stream[Text.Info[Option[A]]] =
- {
- stack match {
- case (parent, (range, (info, tree)) #:: more) :: rest =>
- val subrange = range.restrict(root_range)
- val subtree = tree.overlapping(subrange).toStream
- val start = subrange.start
-
- if (result.isDefinedAt(info)) {
- val next = Text.Info[Option[A]](subrange, Some(result(info)))
- val nexts = stream(start, (next, subtree) :: (parent, more) :: rest)
- if (last < start) parent.restrict(Text.Range(last, start)) #:: nexts
- else nexts
- }
- else stream(last, (parent, subtree #::: more) :: rest)
case (parent, Stream.Empty) :: rest =>
val stop = parent.range.stop
@@ -149,21 +151,25 @@
case Nil =>
val stop = root_range.stop
- if (last < stop) Stream(Text.Info(Text.Range(last, stop), None))
+ if (last < stop) Stream(Text.Info(Text.Range(last, stop), root_info))
else Stream.empty
}
}
stream(root_range.start,
- List((Text.Info(root_range, None), overlapping(root_range).toStream)))
+ List((Text.Info(root_range, root_info), overlapping(root_range).toStream)))
}
def swing_tree(parent: DefaultMutableTreeNode)
(swing_node: Text.Markup => DefaultMutableTreeNode)
{
- for ((_, (info, subtree)) <- branches) {
- val current = swing_node(info)
- subtree.swing_tree(current)(swing_node)
- parent.add(current)
+ for ((_, entry) <- branches) {
+ var current = parent
+ for (info <- entry.markup) {
+ val node = swing_node(Text.Info(entry.range, info))
+ current.add(node)
+ current = node
+ }
+ entry.subtree.swing_tree(current)(swing_node)
}
}
}
--- a/src/Pure/PIDE/text.scala Sat Nov 12 13:01:56 2011 +0100
+++ b/src/Pure/PIDE/text.scala Sat Nov 12 20:14:09 2011 +0100
@@ -115,7 +115,7 @@
catch { case ERROR(_) => None }
}
- type Markup = Info[XML.Tree]
+ type Markup = Info[XML.Elem]
/* editing */
--- a/src/Pure/variable.ML Sat Nov 12 13:01:56 2011 +0100
+++ b/src/Pure/variable.ML Sat Nov 12 20:14:09 2011 +0100
@@ -297,7 +297,6 @@
val fixed_ord = Name_Space.entry_ord o fixes_space;
val intern_fixed = Name_Space.intern o fixes_space;
-val markup_fixed = Name_Space.markup o fixes_space;
fun lookup_fixed ctxt x =
let val x' = intern_fixed ctxt x
@@ -308,6 +307,10 @@
SOME x' => if intern_fixed ctxt x' = x then x' else x
| NONE => x);
+fun markup_fixed ctxt x =
+ Name_Space.markup (fixes_space ctxt) x
+ |> Markup.name (revert_fixed ctxt x);
+
fun dest_fixes ctxt =
let val (space, tab) = fixes_of ctxt
in sort (Name_Space.entry_ord space o pairself #2) (map swap (Symtab.dest tab)) end;
--- a/src/Tools/jEdit/src/document_view.scala Sat Nov 12 13:01:56 2011 +0100
+++ b/src/Tools/jEdit/src/document_view.scala Sat Nov 12 20:14:09 2011 +0100
@@ -293,8 +293,7 @@
else Isabelle.tooltip(tooltips.mkString("\n"))
}
else {
- snapshot.cumulate_markup(Text.Info(range, SortedMap.empty[Long, String]))(
- Isabelle_Markup.tooltip_message) match
+ snapshot.cumulate_markup(range)(Isabelle_Markup.tooltip_message) match
{
case Text.Info(_, msgs) #:: _ if !msgs.isEmpty =>
Isabelle.tooltip(msgs.iterator.map(_._2).mkString("\n"))
--- a/src/Tools/jEdit/src/isabelle_hyperlinks.scala Sat Nov 12 13:01:56 2011 +0100
+++ b/src/Tools/jEdit/src/isabelle_hyperlinks.scala Sat Nov 12 20:14:09 2011 +0100
@@ -57,37 +57,40 @@
case Some(model) =>
val snapshot = model.snapshot()
val markup =
- snapshot.select_markup(Text.Range(buffer_offset, buffer_offset + 1)) {
- // FIXME Isar_Document.Hyperlink extractor
- case Text.Info(info_range,
- XML.Elem(Markup(Markup.ENTITY, props), _))
- if (props.find(
- { case (Markup.KIND, Markup.ML_OPEN) => true
- case (Markup.KIND, Markup.ML_STRUCT) => true
- case _ => false }).isEmpty) =>
- val Text.Range(begin, end) = info_range
- val line = buffer.getLineOfOffset(begin)
- (Position.File.unapply(props), Position.Line.unapply(props)) match {
- case (Some(def_file), Some(def_line)) =>
- new External_Hyperlink(begin, end, line, def_file, def_line)
- case _ if !snapshot.is_outdated =>
- (props, props) match {
- case (Position.Id(def_id), Position.Offset(def_offset)) =>
- snapshot.state.find_command(snapshot.version, def_id) match {
- case Some((def_node, def_cmd)) =>
- def_node.command_start(def_cmd) match {
- case Some(def_cmd_start) =>
- new Internal_Hyperlink(def_cmd.node_name.node, begin, end, line,
- def_cmd_start + def_cmd.decode(def_offset))
+ snapshot.select_markup(Text.Range(buffer_offset, buffer_offset + 1))(
+ Markup_Tree.Select[Hyperlink](
+ {
+ // FIXME Isar_Document.Hyperlink extractor
+ case Text.Info(info_range,
+ XML.Elem(Markup(Markup.ENTITY, props), _))
+ if (props.find(
+ { case (Markup.KIND, Markup.ML_OPEN) => true
+ case (Markup.KIND, Markup.ML_STRUCT) => true
+ case _ => false }).isEmpty) =>
+ val Text.Range(begin, end) = info_range
+ val line = buffer.getLineOfOffset(begin)
+ (Position.File.unapply(props), Position.Line.unapply(props)) match {
+ case (Some(def_file), Some(def_line)) =>
+ new External_Hyperlink(begin, end, line, def_file, def_line)
+ case _ if !snapshot.is_outdated =>
+ (props, props) match {
+ case (Position.Id(def_id), Position.Offset(def_offset)) =>
+ snapshot.state.find_command(snapshot.version, def_id) match {
+ case Some((def_node, def_cmd)) =>
+ def_node.command_start(def_cmd) match {
+ case Some(def_cmd_start) =>
+ new Internal_Hyperlink(def_cmd.node_name.node, begin, end, line,
+ def_cmd_start + def_cmd.decode(def_offset))
+ case None => null
+ }
case None => null
}
- case None => null
+ case _ => null
}
case _ => null
}
- case _ => null
- }
- }
+ },
+ Some(Set(Markup.ENTITY))))
markup match {
case Text.Info(_, Some(link)) #:: _ => link
case _ => null
--- a/src/Tools/jEdit/src/isabelle_markup.scala Sat Nov 12 13:01:56 2011 +0100
+++ b/src/Tools/jEdit/src/isabelle_markup.scala Sat Nov 12 20:14:09 2011 +0100
@@ -87,48 +87,60 @@
/* markup selectors */
- val message: Markup_Tree.Select[Color] =
- {
- case Text.Info(_, XML.Elem(Markup(Markup.WRITELN, _), _)) => regular_color
- case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => warning_color
- case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_color
- }
+ val message =
+ Markup_Tree.Select[Color](
+ {
+ case Text.Info(_, XML.Elem(Markup(Markup.WRITELN, _), _)) => regular_color
+ case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => warning_color
+ case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_color
+ },
+ Some(Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)))
- val tooltip_message: Markup_Tree.Cumulate[SortedMap[Long, String]] =
- {
- case (msgs, Text.Info(_, msg @ XML.Elem(Markup(markup, Markup.Serial(serial)), _)))
- if markup == Markup.WRITELN || markup == Markup.WARNING || markup == Markup.ERROR =>
- msgs + (serial ->
- Pretty.string_of(List(msg), margin = Isabelle.Int_Property("tooltip-margin")))
- }
+ val tooltip_message =
+ Markup_Tree.Cumulate[SortedMap[Long, String]](SortedMap.empty,
+ {
+ case (msgs, Text.Info(_, msg @ XML.Elem(Markup(markup, Markup.Serial(serial)), _)))
+ if markup == Markup.WRITELN || markup == Markup.WARNING || markup == Markup.ERROR =>
+ msgs + (serial ->
+ Pretty.string_of(List(msg), margin = Isabelle.Int_Property("tooltip-margin")))
+ },
+ Some(Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)))
- val gutter_message: Markup_Tree.Select[Icon] =
- {
- case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), body)) =>
- body match {
- case List(XML.Elem(Markup(Markup.LEGACY, _), _)) => legacy_icon
- case _ => warning_icon
- }
- case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_icon
- }
+ val gutter_message =
+ Markup_Tree.Select[Icon](
+ {
+ case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), body)) =>
+ body match {
+ case List(XML.Elem(Markup(Markup.LEGACY, _), _)) => legacy_icon
+ case _ => warning_icon
+ }
+ case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_icon
+ },
+ Some(Set(Markup.WARNING, Markup.ERROR)))
- val background1: Markup_Tree.Select[Color] =
- {
- case Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _)) => bad_color
- case Text.Info(_, XML.Elem(Markup(Markup.HILITE, _), _)) => hilite_color
- }
+ val background1 =
+ Markup_Tree.Select[Color](
+ {
+ case Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _)) => bad_color
+ case Text.Info(_, XML.Elem(Markup(Markup.HILITE, _), _)) => hilite_color
+ },
+ Some(Set(Markup.BAD, Markup.HILITE)))
- val background2: Markup_Tree.Select[Color] =
- {
- case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => light_color
- }
+ val background2 =
+ Markup_Tree.Select[Color](
+ {
+ case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => light_color
+ },
+ Some(Set(Markup.TOKEN_RANGE)))
- val foreground: Markup_Tree.Select[Color] =
- {
- case Text.Info(_, XML.Elem(Markup(Markup.STRING, _), _)) => quoted_color
- case Text.Info(_, XML.Elem(Markup(Markup.ALTSTRING, _), _)) => quoted_color
- case Text.Info(_, XML.Elem(Markup(Markup.VERBATIM, _), _)) => quoted_color
- }
+ val foreground =
+ Markup_Tree.Select[Color](
+ {
+ case Text.Info(_, XML.Elem(Markup(Markup.STRING, _), _)) => quoted_color
+ case Text.Info(_, XML.Elem(Markup(Markup.ALTSTRING, _), _)) => quoted_color
+ case Text.Info(_, XML.Elem(Markup(Markup.VERBATIM, _), _)) => quoted_color
+ },
+ Some(Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM)))
private val text_colors: Map[String, Color] =
Map(
@@ -155,10 +167,13 @@
Markup.ML_MALFORMED -> get_color("#FF6A6A"),
Markup.ANTIQ -> get_color("blue"))
- val text_color: Markup_Tree.Select[Color] =
- {
- case Text.Info(_, XML.Elem(Markup(m, _), _)) if text_colors.isDefinedAt(m) => text_colors(m)
- }
+ val text_color =
+ Markup_Tree.Select[Color](
+ {
+ case Text.Info(_, XML.Elem(Markup(m, _), _))
+ if text_colors.isDefinedAt(m) => text_colors(m)
+ },
+ Some(Set() ++ text_colors.keys))
private val tooltips: Map[String, String] =
Map(
@@ -180,29 +195,36 @@
Pretty.string_of(List(Pretty.block(XML.Text(kind) :: Pretty.Break(1) :: body)),
margin = Isabelle.Int_Property("tooltip-margin"))
- val tooltip1: Markup_Tree.Select[String] =
- {
- case Text.Info(_, XML.Elem(Markup.Entity(kind, name), _)) => kind + " " + quote(name)
- case Text.Info(_, XML.Elem(Markup(Markup.ML_TYPING, _), body)) => string_of_typing("ML:", body)
- case Text.Info(_, XML.Elem(Markup(name, _), _))
- if tooltips.isDefinedAt(name) => tooltips(name)
- }
+ val tooltip1 =
+ Markup_Tree.Select[String](
+ {
+ case Text.Info(_, XML.Elem(Markup.Entity(kind, name), _)) => kind + " " + quote(name)
+ case Text.Info(_, XML.Elem(Markup(Markup.ML_TYPING, _), body)) =>
+ string_of_typing("ML:", body)
+ case Text.Info(_, XML.Elem(Markup(name, _), _))
+ if tooltips.isDefinedAt(name) => tooltips(name)
+ },
+ Some(Set(Markup.ENTITY, Markup.ML_TYPING) ++ tooltips.keys))
- val tooltip2: Markup_Tree.Select[String] =
- {
- case Text.Info(_, XML.Elem(Markup(Markup.TYPING, _), body)) => string_of_typing("::", body)
- }
+ val tooltip2 =
+ Markup_Tree.Select[String](
+ {
+ case Text.Info(_, XML.Elem(Markup(Markup.TYPING, _), body)) => string_of_typing("::", body)
+ },
+ Some(Set(Markup.TYPING)))
private val subexp_include =
Set(Markup.SORT, Markup.TYP, Markup.TERM, Markup.PROP, Markup.ML_TYPING, Markup.TOKEN_RANGE,
Markup.ENTITY, Markup.FREE, Markup.SKOLEM, Markup.BOUND, Markup.VAR,
Markup.TFREE, Markup.TVAR, Markup.ML_SOURCE, Markup.DOC_SOURCE)
- val subexp: Markup_Tree.Select[(Text.Range, Color)] =
- {
- case Text.Info(range, XML.Elem(Markup(name, _), _)) if subexp_include(name) =>
- (range, subexp_color)
- }
+ val subexp =
+ Markup_Tree.Select[(Text.Range, Color)](
+ {
+ case Text.Info(range, XML.Elem(Markup(name, _), _)) if subexp_include(name) =>
+ (range, subexp_color)
+ },
+ Some(subexp_include))
/* token markup -- text styles */