# HG changeset patch # User wenzelm # Date 1321045747 -3600 # Node ID 98af01f897c98de7cf455063c18977bf7c70e673 # Parent 77c5b334a7ae607a151dd3e7d5b04c96d6ba2c37# Parent dcd02d1a25d7d495f5cb37d6e85be28167544c13 merged diff -r 77c5b334a7ae -r 98af01f897c9 src/Pure/Isar/proof_context.ML --- 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 *) diff -r 77c5b334a7ae -r 98af01f897c9 src/Pure/PIDE/blob.scala --- 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) } } diff -r 77c5b334a7ae -r 98af01f897c9 src/Pure/PIDE/command.scala --- 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) diff -r 77c5b334a7ae -r 98af01f897c9 src/Pure/PIDE/document.scala --- 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]]] = { diff -r 77c5b334a7ae -r 98af01f897c9 src/Pure/PIDE/markup_tree.scala --- 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) diff -r 77c5b334a7ae -r 98af01f897c9 src/Pure/PIDE/text.scala --- 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 */ diff -r 77c5b334a7ae -r 98af01f897c9 src/Pure/Syntax/syntax_phases.ML --- 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 diff -r 77c5b334a7ae -r 98af01f897c9 src/Pure/goal.ML --- 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)); diff -r 77c5b334a7ae -r 98af01f897c9 src/Pure/variable.ML --- 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*) diff -r 77c5b334a7ae -r 98af01f897c9 src/Tools/jEdit/src/document_view.scala --- 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 } } diff -r 77c5b334a7ae -r 98af01f897c9 src/Tools/jEdit/src/isabelle_markup.scala --- 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, diff -r 77c5b334a7ae -r 98af01f897c9 src/Tools/jEdit/src/isabelle_sidekick.scala --- 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', ' ')