--- a/NEWS Mon Aug 23 11:57:22 2010 +0200
+++ b/NEWS Mon Aug 23 11:57:32 2010 +0200
@@ -35,6 +35,8 @@
*** HOL ***
+* Dropped type classes mult_mono and mult_mono1. INCOMPATIBILITY.
+
* Theory SetsAndFunctions has been split into Function_Algebras and Set_Algebras;
canonical names for instance definitions for functions; various improvements.
INCOMPATIBILITY.
--- a/src/HOL/Library/Convex.thy Mon Aug 23 11:57:22 2010 +0200
+++ b/src/HOL/Library/Convex.thy Mon Aug 23 11:57:32 2010 +0200
@@ -244,7 +244,7 @@
shows "convex_on s (\<lambda>x. c * f x)"
proof-
have *:"\<And>u c fx v fy ::real. u * (c * fx) + v * (c * fy) = c * (u * fx + v * fy)" by (simp add: field_simps)
- show ?thesis using assms(2) and mult_mono1[OF _ assms(1)] unfolding convex_on_def and * by auto
+ show ?thesis using assms(2) and mult_left_mono [OF _ assms(1)] unfolding convex_on_def and * by auto
qed
lemma convex_lower:
@@ -253,7 +253,7 @@
proof-
let ?m = "max (f x) (f y)"
have "u * f x + v * f y \<le> u * max (f x) (f y) + v * max (f x) (f y)"
- using assms(4,5) by(auto simp add: mult_mono1 add_mono)
+ using assms(4,5) by (auto simp add: mult_left_mono add_mono)
also have "\<dots> = max (f x) (f y)" using assms(6) unfolding distrib[THEN sym] by auto
finally show ?thesis
using assms unfolding convex_on_def by fastsimp
@@ -481,8 +481,8 @@
hence xpos: "?x \<in> C" using asm unfolding convex_alt by fastsimp
have geq: "\<mu> * (f x - f ?x) + (1 - \<mu>) * (f y - f ?x)
\<ge> \<mu> * f' ?x * (x - ?x) + (1 - \<mu>) * f' ?x * (y - ?x)"
- using add_mono[OF mult_mono1[OF leq[OF xpos asm(2)] `\<mu> \<ge> 0`]
- mult_mono1[OF leq[OF xpos asm(3)] `1 - \<mu> \<ge> 0`]] by auto
+ using add_mono[OF mult_left_mono[OF leq[OF xpos asm(2)] `\<mu> \<ge> 0`]
+ mult_left_mono[OF leq[OF xpos asm(3)] `1 - \<mu> \<ge> 0`]] by auto
hence "\<mu> * f x + (1 - \<mu>) * f y - f ?x \<ge> 0"
by (auto simp add:field_simps)
thus "f (\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y) \<le> \<mu> * f x + (1 - \<mu>) * f y"
--- a/src/HOL/Library/Function_Algebras.thy Mon Aug 23 11:57:22 2010 +0200
+++ b/src/HOL/Library/Function_Algebras.thy Mon Aug 23 11:57:32 2010 +0200
@@ -105,12 +105,6 @@
instance "fun" :: (type, mult_zero) mult_zero proof
qed (simp_all add: zero_fun_def times_fun_def)
-instance "fun" :: (type, mult_mono) mult_mono proof
-qed (auto simp add: zero_fun_def times_fun_def le_fun_def intro: mult_left_mono mult_right_mono)
-
-instance "fun" :: (type, mult_mono1) mult_mono1 proof
-qed (auto simp add: zero_fun_def times_fun_def le_fun_def intro: mult_mono1)
-
instance "fun" :: (type, zero_neq_one) zero_neq_one proof
qed (simp add: zero_fun_def one_fun_def expand_fun_eq)
@@ -186,9 +180,11 @@
instance "fun" :: (type, ordered_ab_group_add) ordered_ab_group_add ..
-instance "fun" :: (type, ordered_semiring) ordered_semiring ..
+instance "fun" :: (type, ordered_semiring) ordered_semiring proof
+qed (auto simp add: zero_fun_def times_fun_def le_fun_def intro: mult_left_mono mult_right_mono)
-instance "fun" :: (type, ordered_comm_semiring) ordered_comm_semiring ..
+instance "fun" :: (type, ordered_comm_semiring) ordered_comm_semiring proof
+qed (fact mult_left_mono)
instance "fun" :: (type, ordered_cancel_semiring) ordered_cancel_semiring ..
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Mon Aug 23 11:57:22 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Mon Aug 23 11:57:32 2010 +0200
@@ -2507,7 +2507,7 @@
fix i assume i:"i<DIM('a)" thus "0 < x $$ i" using as[THEN spec[where x="x - (e / 2) *\<^sub>R basis i"]] and `e>0`
unfolding dist_norm by(auto simp add: inner_simps euclidean_component_def dot_basis elim!:allE[where x=i])
next have **:"dist x (x + (e / 2) *\<^sub>R basis 0) < e" using `e>0`
- unfolding dist_norm by(auto intro!: mult_strict_left_mono_comm)
+ unfolding dist_norm by(auto intro!: mult_strict_left_mono)
have "\<And>i. i<DIM('a) \<Longrightarrow> (x + (e / 2) *\<^sub>R basis 0) $$ i = x$$i + (if i = 0 then e/2 else 0)"
unfolding euclidean_component_def by(auto simp add:inner_simps dot_basis)
hence *:"setsum (op $$ (x + (e / 2) *\<^sub>R basis 0)) {..<DIM('a)} = setsum (\<lambda>i. x$$i + (if 0 = i then e/2 else 0)) {..<DIM('a)}"
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Mon Aug 23 11:57:22 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Mon Aug 23 11:57:32 2010 +0200
@@ -220,7 +220,7 @@
fixes x :: "'a::real_normed_vector"
shows "b >= norm(x) ==> \<bar>c\<bar> * b >= norm(scaleR c x)"
unfolding norm_scaleR
- apply (erule mult_mono1)
+ apply (erule mult_left_mono)
apply simp
done
--- a/src/HOL/Multivariate_Analysis/Operator_Norm.thy Mon Aug 23 11:57:22 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Operator_Norm.thy Mon Aug 23 11:57:32 2010 +0200
@@ -107,7 +107,7 @@
apply (subst mult_assoc)
apply (rule order_trans)
apply (rule onorm(1)[OF lf])
- apply (rule mult_mono1)
+ apply (rule mult_left_mono)
apply (rule onorm(1)[OF lg])
apply (rule onorm_pos_le[OF lf])
done
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Aug 23 11:57:22 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Aug 23 11:57:32 2010 +0200
@@ -5678,7 +5678,7 @@
next
case (Suc m)
hence "c * dist (z m) (z (Suc m)) \<le> c ^ Suc m * d"
- using `0 \<le> c` using mult_mono1_class.mult_mono1[of "dist (z m) (z (Suc m))" "c ^ m * d" c] by auto
+ using `0 \<le> c` using mult_left_mono[of "dist (z m) (z (Suc m))" "c ^ m * d" c] by auto
thus ?case using lipschitz[THEN bspec[where x="z m"], OF z_in_s, THEN bspec[where x="z (Suc m)"], OF z_in_s]
unfolding fzn and mult_le_cancel_left by auto
qed
--- a/src/HOL/NSA/StarDef.thy Mon Aug 23 11:57:22 2010 +0200
+++ b/src/HOL/NSA/StarDef.thy Mon Aug 23 11:57:32 2010 +0200
@@ -925,12 +925,12 @@
done
instance star :: (ordered_comm_semiring) ordered_comm_semiring
-by (intro_classes, transfer, rule mult_mono1_class.mult_mono1)
+by (intro_classes, transfer, rule mult_left_mono)
instance star :: (ordered_cancel_comm_semiring) ordered_cancel_comm_semiring ..
instance star :: (linordered_comm_semiring_strict) linordered_comm_semiring_strict
-by (intro_classes, transfer, rule mult_strict_left_mono_comm)
+by (intro_classes, transfer, rule mult_strict_left_mono)
instance star :: (ordered_ring) ordered_ring ..
instance star :: (ordered_ring_abs) ordered_ring_abs
--- a/src/HOL/Probability/Lebesgue.thy Mon Aug 23 11:57:22 2010 +0200
+++ b/src/HOL/Probability/Lebesgue.thy Mon Aug 23 11:57:32 2010 +0200
@@ -700,7 +700,7 @@
using `a \<in> nnfis f` unfolding nnfis_def by auto
with `0 \<le> z`show ?thesis unfolding nnfis_def mono_convergent_def incseq_def
by (auto intro!: exI[of _ "\<lambda>n w. z * u n w"] exI[of _ "\<lambda>n. z * x n"]
- LIMSEQ_mult LIMSEQ_const psfis_mult mult_mono1)
+ LIMSEQ_mult LIMSEQ_const psfis_mult mult_left_mono)
qed
lemma nnfis_add:
--- a/src/HOL/Rings.thy Mon Aug 23 11:57:22 2010 +0200
+++ b/src/HOL/Rings.thy Mon Aug 23 11:57:32 2010 +0200
@@ -628,10 +628,6 @@
end
-class mult_mono = times + zero + ord +
- assumes mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
- assumes mult_right_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c"
-
text {*
The theory of partially ordered rings is taken from the books:
\begin{itemize}
@@ -645,31 +641,29 @@
\end{itemize}
*}
-class ordered_semiring = mult_mono + semiring_0 + ordered_ab_semigroup_add
+class ordered_semiring = semiring + comm_monoid_add + ordered_ab_semigroup_add +
+ assumes mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
+ assumes mult_right_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c"
begin
lemma mult_mono:
- "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> c
- \<Longrightarrow> a * c \<le> b * d"
+ "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * d"
apply (erule mult_right_mono [THEN order_trans], assumption)
apply (erule mult_left_mono, assumption)
done
lemma mult_mono':
- "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> c
- \<Longrightarrow> a * c \<le> b * d"
+ "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * d"
apply (rule mult_mono)
apply (fast intro: order_trans)+
done
end
-class ordered_cancel_semiring = mult_mono + ordered_ab_semigroup_add
- + semiring + cancel_comm_monoid_add
+class ordered_cancel_semiring = ordered_semiring + cancel_comm_monoid_add
begin
subclass semiring_0_cancel ..
-subclass ordered_semiring ..
lemma mult_nonneg_nonneg: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a * b"
using mult_left_mono [of 0 b a] by simp
@@ -689,7 +683,7 @@
end
-class linordered_semiring = semiring + comm_monoid_add + linordered_cancel_ab_semigroup_add + mult_mono
+class linordered_semiring = ordered_semiring + linordered_cancel_ab_semigroup_add
begin
subclass ordered_cancel_semiring ..
@@ -854,41 +848,38 @@
end
-class mult_mono1 = times + zero + ord +
- assumes mult_mono1: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
-
-class ordered_comm_semiring = comm_semiring_0
- + ordered_ab_semigroup_add + mult_mono1
+class ordered_comm_semiring = comm_semiring_0 + ordered_ab_semigroup_add +
+ assumes comm_mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
begin
subclass ordered_semiring
proof
fix a b c :: 'a
assume "a \<le> b" "0 \<le> c"
- thus "c * a \<le> c * b" by (rule mult_mono1)
+ thus "c * a \<le> c * b" by (rule comm_mult_left_mono)
thus "a * c \<le> b * c" by (simp only: mult_commute)
qed
end
-class ordered_cancel_comm_semiring = comm_semiring_0_cancel
- + ordered_ab_semigroup_add + mult_mono1
+class ordered_cancel_comm_semiring = ordered_comm_semiring + cancel_comm_monoid_add
begin
+subclass comm_semiring_0_cancel ..
subclass ordered_comm_semiring ..
subclass ordered_cancel_semiring ..
end
class linordered_comm_semiring_strict = comm_semiring_0 + linordered_cancel_ab_semigroup_add +
- assumes mult_strict_left_mono_comm: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
+ assumes comm_mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
begin
subclass linordered_semiring_strict
proof
fix a b c :: 'a
assume "a < b" "0 < c"
- thus "c * a < c * b" by (rule mult_strict_left_mono_comm)
+ thus "c * a < c * b" by (rule comm_mult_strict_left_mono)
thus "a * c < b * c" by (simp only: mult_commute)
qed
--- a/src/HOL/Transcendental.thy Mon Aug 23 11:57:22 2010 +0200
+++ b/src/HOL/Transcendental.thy Mon Aug 23 11:57:32 2010 +0200
@@ -2790,7 +2790,7 @@
lemma less_one_imp_sqr_less_one: fixes x :: real assumes "\<bar>x\<bar> < 1" shows "x^2 < 1"
proof -
- from mult_mono1[OF less_imp_le[OF `\<bar>x\<bar> < 1`] abs_ge_zero[of x]]
+ from mult_left_mono[OF less_imp_le[OF `\<bar>x\<bar> < 1`] abs_ge_zero[of x]]
have "\<bar> x^2 \<bar> < 1" using `\<bar> x \<bar> < 1` unfolding numeral_2_eq_2 power_Suc2 by auto
thus ?thesis using zero_le_power2 by auto
qed
--- a/src/Pure/General/linear_set.scala Mon Aug 23 11:57:22 2010 +0200
+++ b/src/Pure/General/linear_set.scala Mon Aug 23 11:57:32 2010 +0200
@@ -143,13 +143,13 @@
private def make_iterator(start: Option[A], which: Map[A, A]): Iterator[A] = new Iterator[A] {
private var next_elem = start
- def hasNext = next_elem.isDefined
- def next =
+ def hasNext(): Boolean = next_elem.isDefined
+ def next(): A =
next_elem match {
case Some(elem) =>
next_elem = which.get(elem)
elem
- case None => throw new NoSuchElementException("next on empty iterator")
+ case None => Iterator.empty.next()
}
}
--- a/src/Pure/General/position.scala Mon Aug 23 11:57:22 2010 +0200
+++ b/src/Pure/General/position.scala Mon Aug 23 11:57:32 2010 +0200
@@ -22,9 +22,9 @@
def get_range(pos: T): Option[Text.Range] =
(get_offset(pos), get_end_offset(pos)) match {
- case (Some(start), Some(stop)) => Some(Text.Range(start, stop))
- case (Some(start), None) => Some(Text.Range(start, start + 1))
- case (None, _) => None
+ case (Some(start), Some(stop)) if start <= stop => Some(Text.Range(start, stop))
+ case (Some(start), None) => Some(Text.Range(start))
+ case (_, _) => None
}
object Id { def unapply(pos: T): Option[Long] = get_id(pos) }
--- a/src/Pure/General/pretty.scala Mon Aug 23 11:57:22 2010 +0200
+++ b/src/Pure/General/pretty.scala Mon Aug 23 11:57:32 2010 +0200
@@ -14,12 +14,14 @@
{
/* markup trees with physical blocks and breaks */
+ def block(body: XML.Body): XML.Tree = Block(2, body)
+
object Block
{
- def apply(i: Int, body: List[XML.Tree]): XML.Tree =
+ def apply(i: Int, body: XML.Body): XML.Tree =
XML.Elem(Markup(Markup.BLOCK, List((Markup.INDENT, Markup.Int(i)))), body)
- def unapply(tree: XML.Tree): Option[(Int, List[XML.Tree])] =
+ def unapply(tree: XML.Tree): Option[(Int, XML.Body)] =
tree match {
case XML.Elem(
Markup(Markup.BLOCK, List((Markup.INDENT, Markup.Int(i)))), body) => Some((i, body))
@@ -45,7 +47,7 @@
/* formatted output */
- private def standard_format(tree: XML.Tree): List[XML.Tree] =
+ private def standard_format(tree: XML.Tree): XML.Body =
tree match {
case XML.Elem(markup, body) => List(XML.Elem(markup, body.flatMap(standard_format)))
case XML.Text(text) =>
@@ -53,12 +55,12 @@
Library.chunks(text).toList.map((s: CharSequence) => XML.Text(s.toString)))
}
- case class Text(tx: List[XML.Tree] = Nil, val pos: Double = 0.0, val nl: Int = 0)
+ case class Text(tx: XML.Body = Nil, val pos: Double = 0.0, val nl: Int = 0)
{
def newline: Text = copy(tx = FBreak :: tx, pos = 0.0, nl = nl + 1)
def string(s: String, len: Double): Text = copy(tx = XML.Text(s) :: tx, pos = pos + len)
def blanks(wd: Int): Text = string(Symbol.spaces(wd), wd.toDouble)
- def content: List[XML.Tree] = tx.reverse
+ def content: XML.Body = tx.reverse
}
private val margin_default = 76
@@ -71,8 +73,8 @@
((s: String) => if (s == "\n") 1.0 else metrics.stringWidth(s) / unit)
}
- def formatted(input: List[XML.Tree], margin: Int = margin_default,
- metric: String => Double = metric_default): List[XML.Tree] =
+ def formatted(input: XML.Body, margin: Int = margin_default,
+ metric: String => Double = metric_default): XML.Body =
{
val breakgain = margin / 20
val emergencypos = margin / 2
@@ -83,7 +85,7 @@
case XML.Text(s) => metric(s)
}
- def breakdist(trees: List[XML.Tree], after: Double): Double =
+ def breakdist(trees: XML.Body, after: Double): Double =
trees match {
case Break(_) :: _ => 0.0
case FBreak :: _ => 0.0
@@ -91,7 +93,7 @@
case Nil => after
}
- def forcenext(trees: List[XML.Tree]): List[XML.Tree] =
+ def forcenext(trees: XML.Body): XML.Body =
trees match {
case Nil => Nil
case FBreak :: _ => trees
@@ -99,7 +101,7 @@
case t :: ts => t :: forcenext(ts)
}
- def format(trees: List[XML.Tree], blockin: Double, after: Double, text: Text): Text =
+ def format(trees: XML.Body, blockin: Double, after: Double, text: Text): Text =
trees match {
case Nil => text
@@ -129,16 +131,16 @@
format(input.flatMap(standard_format), 0.0, 0.0, Text()).content
}
- def string_of(input: List[XML.Tree], margin: Int = margin_default,
+ def string_of(input: XML.Body, margin: Int = margin_default,
metric: String => Double = metric_default): String =
formatted(input, margin, metric).iterator.flatMap(XML.content).mkString
/* unformatted output */
- def unformatted(input: List[XML.Tree]): List[XML.Tree] =
+ def unformatted(input: XML.Body): XML.Body =
{
- def fmt(tree: XML.Tree): List[XML.Tree] =
+ def fmt(tree: XML.Tree): XML.Body =
tree match {
case Block(_, body) => body.flatMap(fmt)
case Break(wd) => List(XML.Text(Symbol.spaces(wd)))
@@ -149,6 +151,6 @@
input.flatMap(standard_format).flatMap(fmt)
}
- def str_of(input: List[XML.Tree]): String =
+ def str_of(input: XML.Body): String =
unformatted(input).iterator.flatMap(XML.content).mkString
}
--- a/src/Pure/Isar/toplevel.scala Mon Aug 23 11:57:22 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,33 +0,0 @@
-/* Title: Pure/Isar/toplevel.scala
- Author: Makarius
-
-Isabelle/Isar toplevel transactions.
-*/
-
-package isabelle
-
-
-object Toplevel
-{
- sealed abstract class Status
- case class Forked(forks: Int) extends Status
- case object Unprocessed extends Status
- case object Finished extends Status
- case object Failed extends Status
-
- def command_status(markup: XML.Body): Status =
- {
- val forks = (0 /: markup) {
- case (i, XML.Elem(Markup(Markup.FORKED, _), _)) => i + 1
- case (i, XML.Elem(Markup(Markup.JOINED, _), _)) => i - 1
- case (i, _) => i
- }
- if (forks != 0) Forked(forks)
- else if (markup.exists { case XML.Elem(Markup(Markup.FAILED, _), _) => true case _ => false })
- Failed
- else if (markup.exists { case XML.Elem(Markup(Markup.FINISHED, _), _) => true case _ => false })
- Finished
- else Unprocessed
- }
-}
-
--- a/src/Pure/PIDE/command.scala Mon Aug 23 11:57:22 2010 +0200
+++ b/src/Pure/PIDE/command.scala Mon Aug 23 11:57:32 2010 +0200
@@ -14,20 +14,11 @@
object Command
{
- case class HighlightInfo(kind: String, sub_kind: Option[String]) {
- override def toString = kind
- }
- case class TypeInfo(ty: String)
- case class RefInfo(file: Option[String], line: Option[Int],
- command_id: Option[Document.Command_ID], offset: Option[Int]) // FIXME Command_ID vs. Exec_ID !?
-
-
-
/** accumulated results from prover **/
case class State(
val command: Command,
- val status: List[XML.Tree],
+ val status: List[Markup],
val reverse_results: List[XML.Tree],
val markup: Markup_Tree)
{
@@ -37,86 +28,31 @@
def add_result(result: XML.Tree): State = copy(reverse_results = result :: reverse_results)
- def add_markup(node: Markup_Tree.Node): State = copy(markup = markup + node)
-
- def markup_root_node: Markup_Tree.Node =
- new Markup_Tree.Node(command.range, XML.Elem(Markup(Markup.STATUS, Nil), status))
- def markup_root: Markup_Tree = markup + markup_root_node
-
-
- /* markup */
-
- lazy val highlight: List[Markup_Tree.Node] =
- {
- markup.filter(_.info match {
- case Command.HighlightInfo(_, _) => true
- case _ => false
- }).flatten(markup_root_node)
- }
+ def add_markup(info: Text.Info[Any]): State = copy(markup = markup + info)
- private lazy val types: List[Markup_Tree.Node] =
- markup.filter(_.info match {
- case Command.TypeInfo(_) => true
- case _ => false }).flatten(markup_root_node)
-
- def type_at(pos: Text.Offset): Option[String] =
- {
- types.find(_.range.contains(pos)) match {
- case Some(t) =>
- t.info match {
- case Command.TypeInfo(ty) => Some(command.source(t.range) + " : " + ty)
- case _ => None
- }
- case None => None
- }
- }
-
- private lazy val refs: List[Markup_Tree.Node] =
- markup.filter(_.info match {
- case Command.RefInfo(_, _, _, _) => true
- case _ => false }).flatten(markup_root_node)
-
- def ref_at(pos: Text.Offset): Option[Markup_Tree.Node] =
- refs.find(_.range.contains(pos))
+ def markup_root_info: Text.Info[Any] =
+ new Text.Info(command.range,
+ XML.Elem(Markup(Markup.STATUS, Nil), status.map(XML.Elem(_, Nil))))
+ def markup_root: Markup_Tree = markup + markup_root_info
/* message dispatch */
def accumulate(message: XML.Tree): Command.State =
message match {
- case XML.Elem(Markup(Markup.STATUS, _), body) => copy(status = body ::: status)
+ case XML.Elem(Markup(Markup.STATUS, _), body) => // FIXME explicit checks!?
+ copy(status = (for (XML.Elem(markup, _) <- body) yield markup) ::: status)
- case XML.Elem(Markup(Markup.REPORT, _), elems) =>
- (this /: elems)((state, elem) =>
- elem match {
- case XML.Elem(Markup(kind, atts), body) if Position.get_id(atts) == Some(command.id) =>
- atts match {
- case Position.Range(range) =>
- if (kind == Markup.ML_TYPING) {
- val info = Pretty.string_of(body, margin = 40)
- state.add_markup(command.decode_range(range, Command.TypeInfo(info)))
- }
- else if (kind == Markup.ML_REF) {
- body match {
- case List(XML.Elem(Markup(Markup.ML_DEF, props), _)) =>
- state.add_markup(
- command.decode_range(range,
- Command.RefInfo(
- Position.get_file(props),
- Position.get_line(props),
- Position.get_id(props),
- Position.get_offset(props))))
- case _ => state
- }
- }
- else {
- state.add_markup(
- command.decode_range(range,
- Command.HighlightInfo(kind, Markup.get_string(Markup.KIND, atts))))
- }
- case _ => state
- }
- case _ => System.err.println("Ignored report message: " + elem); state
+ case XML.Elem(Markup(Markup.REPORT, _), msgs) =>
+ (this /: msgs)((state, msg) =>
+ msg match {
+ case XML.Elem(Markup(name, atts), args)
+ if Position.get_id(atts) == Some(command.id) && Position.get_range(atts).isDefined =>
+ val range = command.decode(Position.get_range(atts).get)
+ val props = atts.filterNot(p => Markup.POSITION_PROPERTIES(p._1))
+ val info = Text.Info[Any](range, XML.Elem(Markup(name, props), args))
+ add_markup(info)
+ case _ => System.err.println("Ignored report message: " + msg); state
})
case _ => add_result(message)
}
@@ -152,15 +88,12 @@
val source: String = span.map(_.source).mkString
def source(range: Text.Range): String = source.substring(range.start, range.stop)
def length: Int = source.length
+
val range: Text.Range = Text.Range(0, length)
lazy val symbol_index = new Symbol.Index(source)
-
-
- /* markup */
-
- def decode_range(range: Text.Range, info: Any): Markup_Tree.Node =
- new Markup_Tree.Node(symbol_index.decode(range), info)
+ def decode(i: Text.Offset): Text.Offset = symbol_index.decode(i)
+ def decode(r: Text.Range): Text.Range = symbol_index.decode(r)
/* accumulated results */
--- a/src/Pure/PIDE/document.scala Mon Aug 23 11:57:22 2010 +0200
+++ b/src/Pure/PIDE/document.scala Mon Aug 23 11:57:32 2010 +0200
@@ -65,11 +65,11 @@
def command_start(cmd: Command): Option[Text.Offset] =
command_starts.find(_._1 == cmd).map(_._2)
- def command_range(i: Text.Offset): Iterator[(Command, Text.Offset)] =
+ def command_range(i: Text.Offset = 0): Iterator[(Command, Text.Offset)] =
command_starts dropWhile { case (cmd, start) => start + cmd.length <= i }
- def command_range(i: Text.Offset, j: Text.Offset): Iterator[(Command, Text.Offset)] =
- command_range(i) takeWhile { case (_, start) => start < j }
+ def command_range(range: Text.Range): Iterator[(Command, Text.Offset)] =
+ command_range(range.start) takeWhile { case (_, start) => start < range.stop }
def command_at(i: Text.Offset): Option[(Command, Text.Offset)] =
{
--- a/src/Pure/PIDE/isar_document.ML Mon Aug 23 11:57:22 2010 +0200
+++ b/src/Pure/PIDE/isar_document.ML Mon Aug 23 11:57:32 2010 +0200
@@ -1,7 +1,7 @@
(* Title: Pure/PIDE/isar_document.ML
Author: Makarius
-Protocol commands for interactive Isar documents.
+Protocol message formats for interactive Isar documents.
*)
structure Isar_Document: sig end =
--- a/src/Pure/PIDE/isar_document.scala Mon Aug 23 11:57:22 2010 +0200
+++ b/src/Pure/PIDE/isar_document.scala Mon Aug 23 11:57:32 2010 +0200
@@ -1,7 +1,7 @@
/* Title: Pure/PIDE/isar_document.scala
Author: Makarius
-Protocol commands for interactive Isar documents.
+Protocol message formats for interactive Isar documents.
*/
package isabelle
@@ -9,7 +9,7 @@
object Isar_Document
{
- /* protocol messages */
+ /* document editing */
object Assign {
def unapply(msg: XML.Tree)
@@ -32,6 +32,28 @@
case _ => None
}
}
+
+
+ /* toplevel transactions */
+
+ sealed abstract class Status
+ case class Forked(forks: Int) extends Status
+ case object Unprocessed extends Status
+ case object Finished extends Status
+ case object Failed extends Status
+
+ def command_status(markup: List[Markup]): Status =
+ {
+ val forks = (0 /: markup) {
+ case (i, Markup(Markup.FORKED, _)) => i + 1
+ case (i, Markup(Markup.JOINED, _)) => i - 1
+ case (i, _) => i
+ }
+ if (forks != 0) Forked(forks)
+ else if (markup.exists(_.name == Markup.FAILED)) Failed
+ else if (markup.exists(_.name == Markup.FINISHED)) Finished
+ else Unprocessed
+ }
}
--- a/src/Pure/PIDE/markup_tree.scala Mon Aug 23 11:57:22 2010 +0200
+++ b/src/Pure/PIDE/markup_tree.scala Mon Aug 23 11:57:32 2010 +0200
@@ -17,26 +17,30 @@
object Markup_Tree
{
- case class Node(val range: Text.Range, val info: Any)
- {
- def contains(that: Node): Boolean = this.range contains that.range
- def intersect(r: Text.Range): Node = Node(range.intersect(r), info)
- }
-
-
- /* branches sorted by quasi-order -- overlapping intervals appear as equivalent */
+ /* branches sorted by quasi-order -- overlapping ranges appear as equivalent */
object Branches
{
- type Entry = (Node, Markup_Tree)
- type T = SortedMap[Node, Entry]
+ type Entry = (Text.Info[Any], Markup_Tree)
+ type T = SortedMap[Text.Range, Entry]
- val empty = SortedMap.empty[Node, Entry](new scala.math.Ordering[Node]
+ val empty = SortedMap.empty[Text.Range, Entry](new scala.math.Ordering[Text.Range]
{
- def compare(x: Node, y: Node): Int = x.range compare y.range
+ def compare(r1: Text.Range, r2: Text.Range): Int = r1 compare r2
})
- def update(branches: T, entries: Entry*): T =
- branches ++ entries.map(e => (e._1 -> e))
+
+ def update(branches: T, entry: Entry): T = branches + (entry._1.range -> entry)
+
+ def overlapping(range: Text.Range, branches: T): T =
+ {
+ val start = Text.Range(range.start)
+ val stop = Text.Range(range.stop)
+ branches.get(stop) match {
+ case Some(end) if range overlaps end._1.range =>
+ update(branches.range(start, stop), end)
+ case _ => branches.range(start, stop)
+ }
+ }
}
val empty = new Markup_Tree(Branches.empty)
@@ -47,95 +51,77 @@
{
import Markup_Tree._
- def + (new_node: Node): Markup_Tree =
+ override def toString =
+ branches.toList.map(_._2) match {
+ case Nil => "Empty"
+ case list => list.mkString("Tree(", ",", ")")
+ }
+
+ def + (new_info: Text.Info[Any]): Markup_Tree =
{
- branches.get(new_node) match {
+ val new_range = new_info.range
+ branches.get(new_range) match {
case None =>
- new Markup_Tree(Branches.update(branches, new_node -> empty))
- case Some((node, subtree)) =>
- if (node.range != new_node.range && node.contains(new_node))
- new Markup_Tree(Branches.update(branches, node -> (subtree + new_node)))
- else if (new_node.contains(branches.head._1) && new_node.contains(branches.last._1))
- new Markup_Tree(Branches.update(Branches.empty, (new_node -> this)))
+ new Markup_Tree(Branches.update(branches, new_info -> empty))
+ case Some((info, subtree)) =>
+ val range = info.range
+ if (range != new_range && range.contains(new_range))
+ new Markup_Tree(Branches.update(branches, info -> (subtree + new_info)))
+ else if (new_range.contains(branches.head._1) && new_range.contains(branches.last._1))
+ new Markup_Tree(Branches.update(Branches.empty, (new_info -> this)))
else {
- var overlapping = Branches.empty
- var rest = branches
- while (rest.isDefinedAt(new_node)) {
- overlapping = Branches.update(overlapping, rest(new_node))
- rest -= new_node
+ val body = Branches.overlapping(new_range, branches)
+ if (body.forall(e => new_range.contains(e._1))) {
+ val rest = (Branches.empty /: branches)((rest, entry) =>
+ if (body.isDefinedAt(entry._1)) rest else rest + entry)
+ new Markup_Tree(Branches.update(rest, new_info -> new Markup_Tree(body)))
}
- if (overlapping.forall(e => new_node.contains(e._1)))
- new Markup_Tree(Branches.update(rest, new_node -> new Markup_Tree(overlapping)))
else { // FIXME split markup!?
- System.err.println("Ignored overlapping markup: " + new_node)
+ System.err.println("Ignored overlapping markup information: " + new_info)
this
}
}
}
}
- // FIXME depth-first with result markup stack
- // FIXME projection to given range
- def flatten(parent: Node): List[Node] =
+ def select[A](root_range: Text.Range)
+ (result: PartialFunction[Text.Info[Any], A])(default: A): Stream[Text.Info[A]] =
{
- val result = new mutable.ListBuffer[Node]
- var offset = parent.range.start
- for ((_, (node, subtree)) <- branches.iterator) {
- if (offset < node.range.start)
- result += new Node(Text.Range(offset, node.range.start), parent.info)
- result ++= subtree.flatten(node)
- offset = node.range.stop
+ def stream(parent: Text.Info[A], bs: Branches.T): Stream[Text.Info[A]] =
+ {
+ val range = parent.range
+ val substream =
+ (for ((info_range, (info, subtree)) <- Branches.overlapping(range, bs).toStream) yield {
+ if (result.isDefinedAt(info)) {
+ val current = Text.Info(info_range.restrict(range), result(info))
+ stream(current, subtree.branches)
+ }
+ else stream(parent.restrict(info_range), subtree.branches)
+ }).flatten
+
+ def padding(last: Text.Offset, s: Stream[Text.Info[A]]): Stream[Text.Info[A]] =
+ s match {
+ case info #:: rest =>
+ val Text.Range(start, stop) = info.range
+ if (last < start)
+ parent.restrict(Text.Range(last, start)) #:: info #:: padding(stop, rest)
+ else info #:: padding(stop, rest)
+ case Stream.Empty =>
+ if (last < range.stop)
+ Stream(parent.restrict(Text.Range(last, range.stop)))
+ else Stream.Empty
+ }
+ if (substream.isEmpty) Stream(parent)
+ else padding(range.start, substream)
}
- if (offset < parent.range.stop)
- result += new Node(Text.Range(offset, parent.range.stop), parent.info)
- result.toList
- }
-
- def filter(pred: Node => Boolean): Markup_Tree =
- {
- val bs = branches.toList.flatMap(entry => {
- val (_, (node, subtree)) = entry
- if (pred(node)) List((node, (node, subtree.filter(pred))))
- else subtree.filter(pred).branches.toList
- })
- new Markup_Tree(Branches.empty ++ bs)
+ stream(Text.Info(root_range, default), branches)
}
- def select[A](range: Text.Range)(sel: PartialFunction[Node, A]): Stream[Node] =
+ def swing_tree(parent: DefaultMutableTreeNode)
+ (swing_node: Text.Info[Any] => DefaultMutableTreeNode)
{
- def stream(parent: Node, bs: Branches.T): Stream[Node] =
- {
- val start = Node(parent.range.start_range, Nil)
- val stop = Node(parent.range.stop_range, Nil)
- val substream =
- (for ((_, (node, subtree)) <- bs.range(start, stop).toStream) yield {
- if (sel.isDefinedAt(node))
- stream(node.intersect(parent.range), subtree.branches)
- else stream(parent, subtree.branches)
- }).flatten
-
- def padding(last: Text.Offset, s: Stream[Node]): Stream[Node] =
- s match {
- case node #:: rest =>
- if (last < node.range.start)
- parent.intersect(Text.Range(last, node.range.start)) #::
- node #:: padding(node.range.stop, rest)
- else node #:: padding(node.range.stop, rest)
- case Stream.Empty => // FIXME
- if (last < parent.range.stop)
- Stream(parent.intersect(Text.Range(last, parent.range.stop)))
- else Stream.Empty
- }
- padding(parent.range.start, substream)
- }
- // FIXME handle disjoint range!?
- stream(Node(range, Nil), branches)
- }
-
- def swing_tree(parent: DefaultMutableTreeNode)(swing_node: Node => DefaultMutableTreeNode)
- {
- for ((_, (node, subtree)) <- branches) {
- val current = swing_node(node)
+ for ((_, (info, subtree)) <- branches) {
+ val current = swing_node(info)
subtree.swing_tree(current)(swing_node)
parent.add(current)
}
--- a/src/Pure/PIDE/text.scala Mon Aug 23 11:57:22 2010 +0200
+++ b/src/Pure/PIDE/text.scala Mon Aug 23 11:57:32 2010 +0200
@@ -15,37 +15,38 @@
type Offset = Int
- /* range: interval with total quasi-ordering */
+ /* range -- with total quasi-ordering */
object Range
{
- object Ordering extends scala.math.Ordering[Range]
- {
- override def compare(r1: Range, r2: Range): Int = r1 compare r2
- }
+ def apply(start: Offset): Range = Range(start, start)
}
sealed case class Range(val start: Offset, val stop: Offset)
{
+ // denotation: {start} Un {i. start < i & i < stop}
require(start <= stop)
+ override def toString = "[" + start.toString + ":" + stop.toString + "]"
+
def map(f: Offset => Offset): Range = Range(f(start), f(stop))
def +(i: Offset): Range = map(_ + i)
- def contains(i: Offset): Boolean = start <= i && i < stop
- def contains(that: Range): Boolean =
- this == that || this.contains(that.start) && that.stop <= this.stop
- def overlaps(that: Range): Boolean =
- this == that || this.contains(that.start) || that.contains(this.start)
- def compare(that: Range): Int =
- if (overlaps(that)) 0
- else if (this.start < that.start) -1
- else 1
+ def -(i: Offset): Range = map(_ - i)
+ def contains(i: Offset): Boolean = start == i || start < i && i < stop
+ def contains(that: Range): Boolean = this.contains(that.start) && that.stop <= this.stop
+ def overlaps(that: Range): Boolean = this.contains(that.start) || that.contains(this.start)
+ def compare(that: Range): Int = if (overlaps(that)) 0 else this.start compare that.start
- def start_range: Range = Range(start, start)
- def stop_range: Range = Range(stop, stop)
+ def restrict(that: Range): Range =
+ Range(this.start max that.start, this.stop min that.stop)
+ }
+
- def intersect(that: Range): Range =
- Range(this.start max that.start, this.stop min that.stop)
+ /* information associated with text range */
+
+ case class Info[A](val range: Text.Range, val info: A)
+ {
+ def restrict(r: Text.Range): Info[A] = Info(range.restrict(r), info)
}
--- a/src/Pure/System/isabelle_process.scala Mon Aug 23 11:57:22 2010 +0200
+++ b/src/Pure/System/isabelle_process.scala Mon Aug 23 11:57:32 2010 +0200
@@ -95,7 +95,7 @@
private val xml_cache = new XML.Cache(131071)
- private def put_result(kind: String, props: List[(String, String)], body: List[XML.Tree])
+ private def put_result(kind: String, props: List[(String, String)], body: XML.Body)
{
if (pid.isEmpty && kind == Markup.INIT)
pid = props.find(_._1 == Markup.PID).map(_._1)
@@ -257,7 +257,7 @@
val default_buffer = new Array[Byte](65536)
var c = -1
- def read_chunk(): List[XML.Tree] =
+ def read_chunk(): XML.Body =
{
//{{{
// chunk size
--- a/src/Pure/System/session.scala Mon Aug 23 11:57:22 2010 +0200
+++ b/src/Pure/System/session.scala Mon Aug 23 11:57:32 2010 +0200
@@ -60,7 +60,7 @@
/** main actor **/
@volatile private var syntax = new Outer_Syntax(system.symbols)
- def current_syntax: Outer_Syntax = syntax
+ def current_syntax(): Outer_Syntax = syntax
@volatile private var global_state = Document.State.init
private def change_state(f: Document.State => Document.State) { global_state = f(global_state) }
--- a/src/Pure/Thy/html.scala Mon Aug 23 11:57:22 2010 +0200
+++ b/src/Pure/Thy/html.scala Mon Aug 23 11:57:32 2010 +0200
@@ -41,7 +41,7 @@
// document markup
- def span(cls: String, body: List[XML.Tree]): XML.Elem =
+ def span(cls: String, body: XML.Body): XML.Elem =
XML.Elem(Markup(SPAN, List((CLASS, cls))), body)
def hidden(txt: String): XML.Elem =
@@ -50,9 +50,9 @@
def sub(txt: String): XML.Elem = XML.elem("sub", List(XML.Text(txt)))
def sup(txt: String): XML.Elem = XML.elem("sup", List(XML.Text(txt)))
- def spans(input: XML.Tree, original_data: Boolean = false): List[XML.Tree] =
+ def spans(input: XML.Tree, original_data: Boolean = false): XML.Body =
{
- def html_spans(tree: XML.Tree): List[XML.Tree] =
+ def html_spans(tree: XML.Tree): XML.Body =
tree match {
case XML.Elem(Markup(name, _), ts) =>
if (original_data)
--- a/src/Pure/Thy/thy_syntax.scala Mon Aug 23 11:57:22 2010 +0200
+++ b/src/Pure/Thy/thy_syntax.scala Mon Aug 23 11:57:32 2010 +0200
@@ -84,7 +84,7 @@
commands.iterator(first).takeWhile(_ != last).toList ::: List(last)
val sources = range.flatMap(_.span.map(_.source))
- val spans0 = parse_spans(session.current_syntax.scan(sources.mkString))
+ val spans0 = parse_spans(session.current_syntax().scan(sources.mkString))
val (before_edit, spans1) =
if (!spans0.isEmpty && first.is_command && first.span == spans0.head)
--- a/src/Pure/build-jars Mon Aug 23 11:57:22 2010 +0200
+++ b/src/Pure/build-jars Mon Aug 23 11:57:32 2010 +0200
@@ -37,7 +37,6 @@
Isar/keyword.scala
Isar/outer_syntax.scala
Isar/parse.scala
- Isar/toplevel.scala
Isar/token.scala
PIDE/command.scala
PIDE/document.scala
--- a/src/Pure/library.scala Mon Aug 23 11:57:22 2010 +0200
+++ b/src/Pure/library.scala Mon Aug 23 11:57:32 2010 +0200
@@ -79,7 +79,7 @@
def next(): CharSequence =
state match {
case Some((s, i)) => { state = next_chunk(i); s }
- case None => throw new NoSuchElementException("next on empty iterator")
+ case None => Iterator.empty.next()
}
}
--- a/src/Tools/jEdit/src/jedit/document_model.scala Mon Aug 23 11:57:22 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_model.scala Mon Aug 23 11:57:32 2010 +0200
@@ -257,14 +257,17 @@
override def markTokens(prev: TokenMarker.LineContext,
handler: TokenHandler, line_segment: Segment): TokenMarker.LineContext =
{
+ // FIXME proper synchronization / thread context (!??)
+ val snapshot = Swing_Thread.now { Document_Model.this.snapshot() }
+
val previous = prev.asInstanceOf[Document_Model.Token_Markup.LineContext]
val line = if (prev == null) 0 else previous.line + 1
val context = new Document_Model.Token_Markup.LineContext(line, previous)
+
val start = buffer.getLineStartOffset(line)
val stop = start + line_segment.count
-
- // FIXME proper synchronization / thread context (!??)
- val snapshot = Swing_Thread.now { Document_Model.this.snapshot() }
+ val range = Text.Range(start, stop)
+ val former_range = snapshot.revert(range)
/* FIXME
for (text_area <- Isabelle.jedit_text_areas(buffer)
@@ -275,35 +278,38 @@
def handle_token(style: Byte, offset: Text.Offset, length: Int) =
handler.handleToken(line_segment, style, offset, length, context)
+ val syntax = session.current_syntax()
+ val token_markup: PartialFunction[Text.Info[Any], Byte] =
+ {
+ case Text.Info(_, XML.Elem(Markup(Markup.COMMAND, List((Markup.NAME, name))), _))
+ if syntax.keyword_kind(name).isDefined =>
+ Document_Model.Token_Markup.command_style(syntax.keyword_kind(name).get)
+
+ case Text.Info(_, XML.Elem(Markup(name, _), _))
+ if Document_Model.Token_Markup.token_style(name) != Token.NULL =>
+ Document_Model.Token_Markup.token_style(name)
+ }
+
var next_x = start
for {
- (command, command_start) <-
- snapshot.node.command_range(snapshot.revert(start), snapshot.revert(stop))
- markup <- snapshot.state(command).highlight
- val Text.Range(abs_start, abs_stop) = snapshot.convert(markup.range + command_start)
- if (abs_stop > start)
- if (abs_start < stop)
+ (command, command_start) <- snapshot.node.command_range(former_range)
+ info <- snapshot.state(command).markup.
+ select((former_range - command_start).restrict(command.range))(token_markup)(Token.NULL)
+ val Text.Range(abs_start, abs_stop) = snapshot.convert(info.range + command_start)
+ if abs_stop > start && abs_start < stop // FIXME abs_range overlaps range (redundant!?)
+ }
+ {
val token_start = (abs_start - start) max 0
val token_length =
(abs_stop - abs_start) -
((start - abs_start) max 0) -
((abs_stop - stop) max 0)
- }
- {
- val token_type =
- markup.info match {
- case Command.HighlightInfo(Markup.COMMAND, Some(kind)) =>
- Document_Model.Token_Markup.command_style(kind)
- case Command.HighlightInfo(kind, _) =>
- Document_Model.Token_Markup.token_style(kind)
- case _ => Token.NULL
- }
- if (start + token_start > next_x)
+ if (start + token_start > next_x) // FIXME ??
handle_token(Token.COMMENT1, next_x - start, start + token_start - next_x)
- handle_token(token_type, token_start, token_length)
+ handle_token(info.info, token_start, token_length)
next_x = start + token_start + token_length
}
- if (next_x < stop)
+ if (next_x < stop) // FIXME ??
handle_token(Token.COMMENT1, next_x - start, stop - next_x)
handle_token(Token.END, line_segment.count, 0)
--- a/src/Tools/jEdit/src/jedit/document_view.scala Mon Aug 23 11:57:22 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala Mon Aug 23 11:57:32 2010 +0200
@@ -29,11 +29,11 @@
val state = snapshot.state(command)
if (snapshot.is_outdated) new Color(240, 240, 240)
else
- Toplevel.command_status(state.status) match {
- case Toplevel.Forked(i) if i > 0 => new Color(255, 228, 225)
- case Toplevel.Finished => new Color(234, 248, 255)
- case Toplevel.Failed => new Color(255, 193, 193)
- case Toplevel.Unprocessed => new Color(255, 228, 225)
+ Isar_Document.command_status(state.status) match {
+ case Isar_Document.Forked(i) if i > 0 => new Color(255, 228, 225)
+ case Isar_Document.Finished => new Color(234, 248, 255)
+ case Isar_Document.Failed => new Color(255, 193, 193)
+ case Isar_Document.Unprocessed => new Color(255, 228, 225)
case _ => Color.red
}
}
@@ -202,10 +202,12 @@
val offset = snapshot.revert(text_area.xyToOffset(x, y))
snapshot.node.command_at(offset) match {
case Some((command, command_start)) =>
- snapshot.state(command).type_at(offset - command_start) match {
- case Some(text) => Isabelle.tooltip(text)
- case None => null
- }
+ (snapshot.state(command).markup.select(Text.Range(offset) - command_start) {
+ case Text.Info(range, XML.Elem(Markup(Markup.ML_TYPING, _), body)) =>
+ val typing =
+ Pretty.block(XML.Text(command.source(range) + " : ") :: Pretty.Break(1) :: body)
+ Isabelle.tooltip(Pretty.string_of(List(typing), margin = 40))
+ } { null }).head.info
case None => null
}
}
--- a/src/Tools/jEdit/src/jedit/html_panel.scala Mon Aug 23 11:57:22 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/html_panel.scala Mon Aug 23 11:57:32 2010 +0200
@@ -116,7 +116,7 @@
/* internal messages */
private case class Resize(font_family: String, font_size: Int)
- private case class Render(body: List[XML.Tree])
+ private case class Render(body: XML.Body)
private case object Refresh
private val main_actor = actor {
@@ -127,7 +127,7 @@
var current_font_family = ""
var current_font_size: Int = 0
var current_margin: Int = 0
- var current_body: List[XML.Tree] = Nil
+ var current_body: XML.Body = Nil
def resize(font_family: String, font_size: Int)
{
@@ -152,7 +152,7 @@
def refresh() { render(current_body) }
- def render(body: List[XML.Tree])
+ def render(body: XML.Body)
{
current_body = body
val html_body =
@@ -190,5 +190,5 @@
def resize(font_family: String, font_size: Int) { main_actor ! Resize(font_family, font_size) }
def refresh() { main_actor ! Refresh }
- def render(body: List[XML.Tree]) { main_actor ! Render(body) }
+ def render(body: XML.Body) { main_actor ! Render(body) }
}
--- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Mon Aug 23 11:57:22 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Mon Aug 23 11:57:32 2010 +0200
@@ -38,37 +38,41 @@
class Isabelle_Hyperlinks extends HyperlinkSource
{
- def getHyperlink(buffer: Buffer, original_offset: Int): Hyperlink =
+ def getHyperlink(buffer: Buffer, buffer_offset: Int): Hyperlink =
{
Swing_Thread.assert()
Document_Model(buffer) match {
case Some(model) =>
val snapshot = model.snapshot()
- val offset = snapshot.revert(original_offset)
+ val offset = snapshot.revert(buffer_offset)
snapshot.node.command_at(offset) match {
case Some((command, command_start)) =>
- snapshot.state(command).ref_at(offset - command_start) match {
- case Some(ref) =>
- val Text.Range(begin, end) = snapshot.convert(ref.range + command_start)
+ (snapshot.state(command).markup.select(Text.Range(offset) - command_start) {
+ case Text.Info(info_range, XML.Elem(Markup(Markup.ML_REF, _),
+ List(XML.Elem(Markup(Markup.ML_DEF, props), _)))) =>
+ val Text.Range(begin, end) = snapshot.convert(info_range + command_start)
val line = buffer.getLineOfOffset(begin)
- ref.info match {
- case Command.RefInfo(Some(ref_file), Some(ref_line), _, _) =>
+
+ (Position.get_file(props), Position.get_line(props)) match {
+ case (Some(ref_file), Some(ref_line)) =>
new External_Hyperlink(begin, end, line, ref_file, ref_line)
- case Command.RefInfo(_, _, Some(id), Some(offset)) =>
- snapshot.lookup_command(id) match { // FIXME Command_ID vs. Exec_ID (!??)
- case Some(ref_cmd) =>
- snapshot.node.command_start(ref_cmd) match {
- case Some(ref_cmd_start) =>
- new Internal_Hyperlink(begin, end, line,
- snapshot.convert(ref_cmd_start + offset - 1))
- case None => null // FIXME external ref
+ case _ =>
+ (Position.get_id(props), Position.get_offset(props)) match {
+ case (Some(ref_id), Some(ref_offset)) =>
+ snapshot.lookup_command(ref_id) match {
+ case Some(ref_cmd) =>
+ snapshot.node.command_start(ref_cmd) match {
+ case Some(ref_cmd_start) =>
+ new Internal_Hyperlink(begin, end, line,
+ snapshot.convert(ref_cmd_start + ref_cmd.decode(ref_offset)))
+ case None => null
+ }
+ case None => null
}
case _ => null
}
- case _ => null
}
- case None => null
- }
+ } { null }).head.info
case None => null
}
case None => null
--- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Mon Aug 23 11:57:22 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Mon Aug 23 11:57:32 2010 +0200
@@ -72,7 +72,7 @@
val start = buffer.getLineStartOffset(line)
val text = buffer.getSegment(start, caret - start)
- val completion = Isabelle.session.current_syntax.completion
+ val completion = Isabelle.session.current_syntax().completion
completion.complete(text) match {
case None => null
@@ -97,7 +97,7 @@
val root = data.root
val snapshot = Swing_Thread.now { model.snapshot() } // FIXME cover all nodes (!??)
for {
- (command, command_start) <- snapshot.node.command_range(0)
+ (command, command_start) <- snapshot.node.command_range()
if command.is_command && !stopped
}
{
@@ -128,22 +128,22 @@
val root = data.root
val snapshot = Swing_Thread.now { model.snapshot() } // FIXME cover all nodes (!??)
- for ((command, command_start) <- snapshot.node.command_range(0) if !stopped) {
- snapshot.state(command).markup_root.swing_tree(root)((node: Markup_Tree.Node) =>
+ for ((command, command_start) <- snapshot.node.command_range() if !stopped) {
+ snapshot.state(command).markup_root.swing_tree(root)((info: Text.Info[Any]) =>
{
- val content = command.source(node.range).replace('\n', ' ')
+ val content = command.source(info.range).replace('\n', ' ')
val id = command.id
new DefaultMutableTreeNode(new IAsset {
override def getIcon: Icon = null
override def getShortString: String = content
- override def getLongString: String = node.info.toString
+ override def getLongString: String = info.info.toString
override def getName: String = Markup.Long(id)
override def setName(name: String) = ()
override def setStart(start: Position) = ()
- override def getStart: Position = command_start + node.range.start
+ override def getStart: Position = command_start + info.range.start
override def setEnd(end: Position) = ()
- override def getEnd: Position = command_start + node.range.stop
+ override def getEnd: Position = command_start + info.range.stop
override def toString = id + ": " + content + "[" + getStart + " - " + getEnd + "]"
})
})