--- a/src/Pure/Isar/proof_context.ML Fri Nov 11 12:31:00 2011 +0100
+++ b/src/Pure/Isar/proof_context.ML Fri Nov 11 22:09:07 2011 +0100
@@ -71,7 +71,7 @@
val read_const_proper: Proof.context -> bool -> string -> term
val read_const: Proof.context -> bool -> typ -> string -> term
val allow_dummies: Proof.context -> Proof.context
- val get_sort: Proof.context -> (indexname * sort) list -> indexname -> sort
+ val prepare_sorts: Proof.context -> typ list -> typ list
val check_tfree: Proof.context -> string * sort -> string * sort
val intern_skolem: Proof.context -> string -> string option
val read_term_pattern: Proof.context -> string -> term
@@ -613,35 +613,47 @@
(* sort constraints *)
-fun get_sort ctxt raw_text =
+fun prepare_sorts ctxt tys =
let
val tsig = tsig_of ctxt;
-
- val text = distinct (op =) (map (apsnd (Type.minimize_sort tsig)) raw_text);
- val _ =
- (case duplicates (eq_fst (op =)) text of
- [] => ()
- | dups => error ("Inconsistent sort constraints for type variable(s) "
- ^ commas_quote (map (Term.string_of_vname' o fst) dups)));
+ val defaultS = Type.defaultS tsig;
- fun lookup xi =
- (case AList.lookup (op =) text xi of
- NONE => NONE
- | SOME S => if S = dummyS then NONE else SOME S);
+ fun constraint (xi, S) env =
+ if S = dummyS then env
+ else
+ Vartab.insert (op =) (xi, Type.minimize_sort tsig S) env
+ handle Vartab.DUP _ =>
+ error ("Inconsistent sort constraints for type variable " ^
+ quote (Term.string_of_vname' xi));
+ val env =
+ (fold o fold_atyps)
+ (fn TFree (x, S) => constraint ((x, ~1), S)
+ | TVar v => constraint v
+ | _ => I) tys Vartab.empty;
- fun get xi =
- (case (lookup xi, Variable.def_sort ctxt xi) of
- (NONE, NONE) => Type.defaultS tsig
+ fun get_sort xi =
+ (case (Vartab.lookup env xi, Variable.def_sort ctxt xi) of
+ (NONE, NONE) => defaultS
| (NONE, SOME S) => S
| (SOME S, NONE) => S
| (SOME S, SOME S') =>
if Type.eq_sort tsig (S, S') then S'
- else error ("Sort constraint " ^ Syntax.string_of_sort ctxt S ^
- " inconsistent with default " ^ Syntax.string_of_sort ctxt S' ^
- " for type variable " ^ quote (Term.string_of_vname' xi)));
- in get end;
+ else
+ error ("Sort constraint " ^ Syntax.string_of_sort ctxt S ^
+ " inconsistent with default " ^ Syntax.string_of_sort ctxt S' ^
+ " for type variable " ^ quote (Term.string_of_vname' xi)));
+ in
+ (map o map_atyps)
+ (fn T =>
+ if Term_Position.is_positionT T then T
+ else
+ (case T of
+ TFree (x, _) => TFree (x, get_sort (x, ~1))
+ | TVar (xi, _) => TVar (xi, get_sort xi)
+ | _ => T)) tys
+ end;
-fun check_tfree ctxt (x, S) = (x, get_sort ctxt [((x, ~1), S)] (x, ~1));
+fun check_tfree ctxt v = dest_TFree (singleton (prepare_sorts ctxt) (TFree v));
(* certify terms *)
--- a/src/Pure/PIDE/blob.scala Fri Nov 11 12:31:00 2011 +0100
+++ b/src/Pure/PIDE/blob.scala Fri Nov 11 22:09:07 2011 +0100
@@ -11,7 +11,7 @@
{
sealed case class State(val blob: Blob, val markup: Markup_Tree = Markup_Tree.empty)
{
- def + (info: Text.Info[Any]): State = copy(markup = markup + info)
+ def + (info: Text.Markup): State = copy(markup = markup + info)
}
}
--- a/src/Pure/PIDE/command.scala Fri Nov 11 12:31:00 2011 +0100
+++ b/src/Pure/PIDE/command.scala Fri Nov 11 22:09:07 2011 +0100
@@ -25,12 +25,12 @@
/* content */
def add_status(st: Markup): State = copy(status = st :: status)
- def add_markup(info: Text.Info[Any]): State = copy(markup = markup + info)
+ def add_markup(m: Text.Markup): State = copy(markup = markup + m)
def add_result(serial: Long, result: XML.Tree): State =
copy(results = results + (serial -> result))
- def root_info: Text.Info[Any] =
- new Text.Info(command.range,
+ def root_info: Text.Markup =
+ Text.Info(command.range,
XML.Elem(Markup(Markup.STATUS, Nil), status.reverse.map(XML.Elem(_, Nil))))
def root_markup: Markup_Tree = markup + root_info
@@ -53,7 +53,7 @@
if id == command.id && command.range.contains(command.decode(raw_range)) =>
val range = command.decode(raw_range)
val props = Position.purge(atts)
- val info = Text.Info[Any](range, XML.Elem(Markup(name, props), args))
+ val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args))
state.add_markup(info)
case _ =>
// FIXME System.err.println("Ignored report message: " + msg)
--- a/src/Pure/PIDE/document.scala Fri Nov 11 12:31:00 2011 +0100
+++ b/src/Pure/PIDE/document.scala Fri Nov 11 22:09:07 2011 +0100
@@ -240,6 +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])
: Stream[Text.Info[Option[A]]]
}
@@ -471,6 +473,21 @@
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])
+ : Stream[Text.Info[A]] =
+ {
+ val former_range = revert(root.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)))
+ }
+ } yield Text.Info(convert(r0 + command_start), a)
+ }
+
def select_markup[A](range: Text.Range)(result: Markup_Tree.Select[A])
: Stream[Text.Info[Option[A]]] =
{
--- a/src/Pure/PIDE/markup_tree.scala Fri Nov 11 12:31:00 2011 +0100
+++ b/src/Pure/PIDE/markup_tree.scala Fri Nov 11 22:09:07 2011 +0100
@@ -15,37 +15,24 @@
object Markup_Tree
{
- /* branches sorted by quasi-order -- overlapping ranges appear as equivalent */
+ type Cumulate[A] = PartialFunction[(A, Text.Markup), A]
+ type Select[A] = PartialFunction[Text.Markup, A]
+
+ val empty: Markup_Tree = new Markup_Tree(Branches.empty)
object Branches
{
- type Entry = (Text.Info[Any], Markup_Tree)
+ type Entry = (Text.Markup, Markup_Tree)
type T = SortedMap[Text.Range, Entry]
- val empty = SortedMap.empty[Text.Range, Entry](Text.Range.Ordering)
-
+ 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)
-
- def overlapping(range: Text.Range, branches: T): T = // FIXME special cases!?
- {
- val start = Text.Range(range.start)
- val stop = Text.Range(range.stop)
- val bs = branches.range(start, stop)
- branches.get(stop) match {
- case Some(end) if range overlaps end._1.range => update(bs, end)
- case _ => bs
- }
- }
}
-
- val empty = new Markup_Tree(Branches.empty)
-
- type Select[A] = PartialFunction[Text.Info[Any], A]
}
-sealed case class Markup_Tree(val branches: Markup_Tree.Branches.T)
+class Markup_Tree private(branches: Markup_Tree.Branches.T)
{
import Markup_Tree._
@@ -55,7 +42,19 @@
case list => list.mkString("Tree(", ",", ")")
}
- def + (new_info: Text.Info[Any]): Markup_Tree =
+ private def overlapping(range: Text.Range): Branches.T = // FIXME special cases!?
+ {
+ 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 _ => bs
+ }
+ }
+
+ def + (new_info: Text.Markup): Markup_Tree =
{
val new_range = new_info.range
branches.get(new_range) match {
@@ -68,7 +67,7 @@
else if (new_range.contains(branches.head._1) && new_range.contains(branches.last._1))
new Markup_Tree(Branches.single(new_info -> this))
else {
- val body = Branches.overlapping(new_range, branches)
+ 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
if (body.size > 1)
@@ -85,11 +84,43 @@
}
}
- private def overlapping(range: Text.Range): Stream[(Text.Range, Branches.Entry)] =
- Branches.overlapping(range, branches).toStream
+ def cumulate[A](root: Text.Info[A])(result: Cumulate[A]): Stream[Text.Info[A]] =
+ {
+ def stream(
+ last: Text.Offset,
+ stack: List[(Text.Info[A], Stream[(Text.Range, Branches.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
+ val start = subrange.start
- def select[A](root_range: Text.Range)(result: Markup_Tree.Select[A])
- : Stream[Text.Info[Option[A]]] =
+ 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
+ }
+ 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,
@@ -99,7 +130,7 @@
stack match {
case (parent, (range, (info, tree)) #:: more) :: rest =>
val subrange = range.restrict(root_range)
- val subtree = tree.overlapping(subrange)
+ val subtree = tree.overlapping(subrange).toStream
val start = subrange.start
if (result.isDefinedAt(info)) {
@@ -122,11 +153,12 @@
else Stream.empty
}
}
- stream(root_range.start, List((Text.Info(root_range, None), overlapping(root_range))))
+ stream(root_range.start,
+ List((Text.Info(root_range, None), overlapping(root_range).toStream)))
}
def swing_tree(parent: DefaultMutableTreeNode)
- (swing_node: Text.Info[Any] => DefaultMutableTreeNode)
+ (swing_node: Text.Markup => DefaultMutableTreeNode)
{
for ((_, (info, subtree)) <- branches) {
val current = swing_node(info)
--- a/src/Pure/PIDE/text.scala Fri Nov 11 12:31:00 2011 +0100
+++ b/src/Pure/PIDE/text.scala Fri Nov 11 22:09:07 2011 +0100
@@ -115,6 +115,8 @@
catch { case ERROR(_) => None }
}
+ type Markup = Info[XML.Tree]
+
/* editing */
--- a/src/Pure/Syntax/syntax_phases.ML Fri Nov 11 12:31:00 2011 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML Fri Nov 11 22:09:07 2011 +0100
@@ -59,7 +59,7 @@
fun markup_var xi = [Markup.name (Term.string_of_vname xi) Markup.var];
fun markup_bound def ps (name, id) =
- let val entity = Markup.entity "bound variable" name in
+ let val entity = Markup.entity Markup.boundN name in
Markup.bound ::
map (fn pos => Markup.properties (Position.entity_properties_of def id pos) entity) ps
end;
@@ -155,12 +155,8 @@
in [Ast.Constant (Lexicon.mark_type c)] end
| asts_of (Parser.Node ("_position", [pt as Parser.Tip tok])) =
if constrain_pos then
- let val pos = Lexicon.pos_of_token tok in
- if Position.is_reported pos then
- [Ast.Appl [Ast.Constant "_constrain", ast_of pt,
- Ast.Variable (Term_Position.encode pos)]]
- else [ast_of pt]
- end
+ [Ast.Appl [Ast.Constant "_constrain", ast_of pt,
+ Ast.Variable (Term_Position.encode (Lexicon.pos_of_token tok))]]
else [ast_of pt]
| asts_of (Parser.Node (a, pts)) =
let
@@ -798,37 +794,17 @@
val apply_typ_uncheck = check fst true;
val apply_term_uncheck = check snd true;
-fun prepare_sorts ctxt tys =
- let
- fun constraint (xi: indexname, S) = S <> dummyS ? insert (op =) (xi, S);
- val env =
- (fold o fold_atyps)
- (fn TFree (x, S) => constraint ((x, ~1), S)
- | TVar v => constraint v
- | _ => I) tys [];
- val get_sort = Proof_Context.get_sort ctxt env;
- in
- (map o map_atyps)
- (fn T =>
- if Term_Position.is_positionT T then T
- else
- (case T of
- TFree (x, _) => TFree (x, get_sort (x, ~1))
- | TVar (xi, _) => TVar (xi, get_sort xi)
- | _ => T)) tys
- end;
-
in
fun check_typs ctxt =
- prepare_sorts ctxt #>
+ Proof_Context.prepare_sorts ctxt #>
apply_typ_check ctxt #>
Term_Sharing.typs (Proof_Context.theory_of ctxt);
fun check_terms ctxt raw_ts =
let
val (ts, ps) = raw_ts
- |> Term.burrow_types (prepare_sorts ctxt)
+ |> Term.burrow_types (Proof_Context.prepare_sorts ctxt)
|> Type_Infer_Context.prepare_positions ctxt;
val tys = map (Logic.mk_type o snd) ps;
val (ts', tys') = ts @ tys
--- a/src/Pure/goal.ML Fri Nov 11 12:31:00 2011 +0100
+++ b/src/Pure/goal.ML Fri Nov 11 22:09:07 2011 +0100
@@ -125,7 +125,7 @@
val _ = forked 1;
val future =
(singleton o Future.forks)
- {name = name, group = NONE, deps = [], pri = ~1, interrupts = false}
+ {name = name, group = NONE, deps = [], pri = 0, interrupts = false}
(fn () =>
Exn.release
(Exn.capture (Future.status o Future.interruptible_task) e before forked ~1));
--- a/src/Pure/variable.ML Fri Nov 11 12:31:00 2011 +0100
+++ b/src/Pure/variable.ML Fri Nov 11 22:09:07 2011 +0100
@@ -81,7 +81,7 @@
(** local context data **)
type fixes = string Name_Space.table;
-val empty_fixes: fixes = Name_Space.empty_table "fixed variable";
+val empty_fixes: fixes = Name_Space.empty_table Markup.fixedN;
datatype data = Data of
{is_body: bool, (*inner body mode*)
--- a/src/Tools/jEdit/src/document_view.scala Fri Nov 11 12:31:00 2011 +0100
+++ b/src/Tools/jEdit/src/document_view.scala Fri Nov 11 22:09:07 2011 +0100
@@ -11,6 +11,7 @@
import isabelle._
import scala.collection.mutable
+import scala.collection.immutable.SortedMap
import scala.actors.Actor._
import java.lang.System
@@ -274,18 +275,29 @@
robust_body(null: String) {
val snapshot = update_snapshot()
val offset = text_area.xyToOffset(x, y)
+ val range = Text.Range(offset, offset + 1)
+
if (control) {
- snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Markup.tooltip) match
- {
- case Text.Info(_, Some(text)) #:: _ => Isabelle.tooltip(text)
- case _ => null
- }
+ val tooltips =
+ (snapshot.select_markup(range)(Isabelle_Markup.tooltip1) match
+ {
+ case Text.Info(_, Some(text)) #:: _ => List(text)
+ case _ => Nil
+ }) :::
+ (snapshot.select_markup(range)(Isabelle_Markup.tooltip2) match
+ {
+ case Text.Info(_, Some(text)) #:: _ => List(text)
+ case _ => Nil
+ })
+ if (tooltips.isEmpty) null
+ else Isabelle.tooltip(tooltips.mkString("\n"))
}
else {
- // FIXME snapshot.cumulate
- snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Markup.popup) match
+ snapshot.cumulate_markup(Text.Info(range, SortedMap.empty[Long, String]))(
+ Isabelle_Markup.tooltip_message) match
{
- case Text.Info(_, Some(text)) #:: _ => Isabelle.tooltip(text)
+ case Text.Info(_, msgs) #:: _ if !msgs.isEmpty =>
+ Isabelle.tooltip(msgs.iterator.map(_._2).mkString("\n"))
case _ => null
}
}
--- a/src/Tools/jEdit/src/isabelle_markup.scala Fri Nov 11 12:31:00 2011 +0100
+++ b/src/Tools/jEdit/src/isabelle_markup.scala Fri Nov 11 22:09:07 2011 +0100
@@ -14,6 +14,8 @@
import org.lobobrowser.util.gui.ColorFactory
import org.gjt.sp.jedit.syntax.{Token => JEditToken}
+import scala.collection.immutable.SortedMap
+
object Isabelle_Markup
{
@@ -92,11 +94,12 @@
case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_color
}
- val popup: Markup_Tree.Select[String] =
+ val tooltip_message: Markup_Tree.Cumulate[SortedMap[Long, String]] =
{
- case Text.Info(_, msg @ XML.Elem(Markup(markup, _), _))
+ case (msgs, Text.Info(_, msg @ XML.Elem(Markup(markup, Markup.Serial(serial)), _)))
if markup == Markup.WRITELN || markup == Markup.WARNING || markup == Markup.ERROR =>
- Pretty.string_of(List(msg), margin = Isabelle.Int_Property("tooltip-margin"))
+ msgs + (serial ->
+ Pretty.string_of(List(msg), margin = Isabelle.Int_Property("tooltip-margin")))
}
val gutter_message: Markup_Tree.Select[Icon] =
@@ -127,9 +130,6 @@
case Text.Info(_, XML.Elem(Markup(Markup.VERBATIM, _), _)) => quoted_color
}
- private val text_entity_colors: Map[String, Color] =
- Map(Markup.CLASS -> get_color("red"))
-
private val text_colors: Map[String, Color] =
Map(
Markup.STRING -> get_color("black"),
@@ -157,10 +157,7 @@
val text_color: Markup_Tree.Select[Color] =
{
- case Text.Info(_, XML.Elem(Markup.Entity(kind, _), _))
- if text_entity_colors.isDefinedAt(kind) => text_entity_colors(kind)
- case Text.Info(_, XML.Elem(Markup(m, _), _))
- if text_colors.isDefinedAt(m) => text_colors(m)
+ case Text.Info(_, XML.Elem(Markup(m, _), _)) if text_colors.isDefinedAt(m) => text_colors(m)
}
private val tooltips: Map[String, String] =
@@ -170,9 +167,9 @@
Markup.TERM -> "term",
Markup.PROP -> "proposition",
Markup.TOKEN_RANGE -> "inner syntax token",
- Markup.FREE -> "free variable (globally fixed)",
- Markup.SKOLEM -> "skolem variable (locally fixed)",
- Markup.BOUND -> "bound variable (internally fixed)",
+ Markup.FREE -> "free variable",
+ Markup.SKOLEM -> "skolem variable",
+ Markup.BOUND -> "bound variable",
Markup.VAR -> "schematic variable",
Markup.TFREE -> "free type variable",
Markup.TVAR -> "schematic type variable",
@@ -183,15 +180,19 @@
Pretty.string_of(List(Pretty.block(XML.Text(kind) :: Pretty.Break(1) :: body)),
margin = Isabelle.Int_Property("tooltip-margin"))
- val tooltip: Markup_Tree.Select[String] =
+ 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.TYPING, _), body)) => string_of_typing("::", body)
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 tooltip2: Markup_Tree.Select[String] =
+ {
+ case Text.Info(_, XML.Elem(Markup(Markup.TYPING, _), body)) => string_of_typing("::", body)
+ }
+
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,
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala Fri Nov 11 12:31:00 2011 +0100
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Fri Nov 11 22:09:07 2011 +0100
@@ -152,7 +152,7 @@
val root = data.root
val snapshot = Swing_Thread.now { model.snapshot() } // FIXME cover all nodes (!??)
for ((command, command_start) <- snapshot.node.command_range() if !stopped) {
- snapshot.command_state(command).root_markup.swing_tree(root)((info: Text.Info[Any]) =>
+ snapshot.command_state(command).root_markup.swing_tree(root)((info: Text.Markup) =>
{
val range = info.range + command_start
val content = command.source(info.range).replace('\n', ' ')