merged
authorwenzelm
Sat Apr 26 22:57:51 2014 +0200 (2014-04-26)
changeset 56762539fe017905a
parent 56742 678a52e676b6
parent 56761 951c6a9ac3d7
child 56763 70371621fdb6
merged
NEWS
     1.1 --- a/NEWS	Sat Apr 26 14:53:22 2014 +0200
     1.2 +++ b/NEWS	Sat Apr 26 22:57:51 2014 +0200
     1.3 @@ -109,6 +109,9 @@
     1.4  * Document panel: simplied interaction where every single mouse click
     1.5  (re)opens document via desktop environment or as jEdit buffer.
     1.6  
     1.7 +* Find panel: support for 'find_consts' in addition to
     1.8 +'find_theorems'.
     1.9 +
    1.10  * Option "jedit_print_mode" (see also "Plugin Options / Isabelle /
    1.11  General") allows to specify additional print modes for the prover
    1.12  process, without requiring old-fashioned command-line invocation of
     2.1 --- a/src/HOL/Hahn_Banach/Hahn_Banach.thy	Sat Apr 26 14:53:22 2014 +0200
     2.2 +++ b/src/HOL/Hahn_Banach/Hahn_Banach.thy	Sat Apr 26 22:57:51 2014 +0200
     2.3 @@ -391,7 +391,7 @@
     2.4      ultimately show "0 \<le> p x"  
     2.5        by (simp add: p_def zero_le_mult_iff)
     2.6  
     2.7 -    txt {* @{text p} is absolutely homogenous: *}
     2.8 +    txt {* @{text p} is absolutely homogeneous: *}
     2.9  
    2.10      show "p (a \<cdot> x) = \<bar>a\<bar> * p x"
    2.11      proof -
     3.1 --- a/src/HOL/Hahn_Banach/Normed_Space.thy	Sat Apr 26 14:53:22 2014 +0200
     3.2 +++ b/src/HOL/Hahn_Banach/Normed_Space.thy	Sat Apr 26 22:57:51 2014 +0200
     3.3 @@ -13,7 +13,7 @@
     3.4  text {*
     3.5    A \emph{seminorm} @{text "\<parallel>\<cdot>\<parallel>"} is a function on a real vector space
     3.6    into the reals that has the following properties: it is positive
     3.7 -  definite, absolute homogenous and subadditive.
     3.8 +  definite, absolute homogeneous and subadditive.
     3.9  *}
    3.10  
    3.11  locale seminorm =
     4.1 --- a/src/Pure/GUI/gui.scala	Sat Apr 26 14:53:22 2014 +0200
     4.2 +++ b/src/Pure/GUI/gui.scala	Sat Apr 26 22:57:51 2014 +0200
     4.3 @@ -9,10 +9,10 @@
     4.4  
     4.5  
     4.6  import java.lang.{ClassLoader, ClassNotFoundException, NoSuchMethodException}
     4.7 -import java.awt.{Image, Component, Container, Toolkit, Window, Font}
     4.8 +import java.awt.{Image, Component, Container, Toolkit, Window, Font, KeyboardFocusManager}
     4.9  import java.awt.font.{TextAttribute, TransformAttribute, FontRenderContext, LineMetrics}
    4.10  import java.awt.geom.AffineTransform
    4.11 -import javax.swing.{ImageIcon, JOptionPane, UIManager, JLayeredPane, JFrame, JWindow}
    4.12 +import javax.swing.{ImageIcon, JOptionPane, UIManager, JLayeredPane, JFrame, JWindow, JButton}
    4.13  
    4.14  import scala.collection.convert.WrapAsJava
    4.15  import scala.swing.{ComboBox, TextArea, ScrollPane}
    4.16 @@ -39,6 +39,18 @@
    4.17      UIManager.getSystemLookAndFeelClassName() == UIManager.getLookAndFeel.getClass.getName
    4.18  
    4.19  
    4.20 +  /* plain focus traversal, notably for text fields */
    4.21 +
    4.22 +  def plain_focus_traversal(component: Component)
    4.23 +  {
    4.24 +    val dummy_button = new JButton
    4.25 +    def apply(id: Int): Unit =
    4.26 +      component.setFocusTraversalKeys(id, dummy_button.getFocusTraversalKeys(id))
    4.27 +    apply(KeyboardFocusManager.FORWARD_TRAVERSAL_KEYS)
    4.28 +    apply(KeyboardFocusManager.BACKWARD_TRAVERSAL_KEYS)
    4.29 +  }
    4.30 +
    4.31 +
    4.32    /* X11 window manager */
    4.33  
    4.34    def window_manager(): Option[String] =
     5.1 --- a/src/Pure/General/multi_map.scala	Sat Apr 26 14:53:22 2014 +0200
     5.2 +++ b/src/Pure/General/multi_map.scala	Sat Apr 26 22:57:51 2014 +0200
     5.3 @@ -1,5 +1,6 @@
     5.4  /*  Title:      Pure/General/multi_map.scala
     5.5      Module:     PIDE
     5.6 +    Author:     Makarius
     5.7  
     5.8  Maps with multiple entries per key.
     5.9  */
     6.1 --- a/src/Pure/General/position.scala	Sat Apr 26 14:53:22 2014 +0200
     6.2 +++ b/src/Pure/General/position.scala	Sat Apr 26 22:57:51 2014 +0200
     6.3 @@ -83,13 +83,13 @@
     6.4  
     6.5    object Reported
     6.6    {
     6.7 -    def unapply(pos: T): Option[(Long, Text.Chunk.Name, Symbol.Range)] =
     6.8 +    def unapply(pos: T): Option[(Long, Symbol.Text_Chunk.Name, Symbol.Range)] =
     6.9        (pos, pos) match {
    6.10          case (Id(id), Range(range)) =>
    6.11            val chunk_name =
    6.12              pos match {
    6.13 -              case File(name) => Text.Chunk.File(name)
    6.14 -              case _ => Text.Chunk.Default
    6.15 +              case File(name) => Symbol.Text_Chunk.File(name)
    6.16 +              case _ => Symbol.Text_Chunk.Default
    6.17              }
    6.18            Some((id, chunk_name, range))
    6.19          case _ => None
     7.1 --- a/src/Pure/General/symbol.scala	Sat Apr 26 14:53:22 2014 +0200
     7.2 +++ b/src/Pure/General/symbol.scala	Sat Apr 26 22:57:51 2014 +0200
     7.3 @@ -179,6 +179,44 @@
     7.4    }
     7.5  
     7.6  
     7.7 +  /* text chunks */
     7.8 +
     7.9 +  object Text_Chunk
    7.10 +  {
    7.11 +    sealed abstract class Name
    7.12 +    case object Default extends Name
    7.13 +    case class Id(id: Document_ID.Generic) extends Name
    7.14 +    case class File(name: String) extends Name
    7.15 +
    7.16 +    def apply(text: CharSequence): Text_Chunk =
    7.17 +      new Text_Chunk(Text.Range(0, text.length), Index(text))
    7.18 +  }
    7.19 +
    7.20 +  final class Text_Chunk private(val range: Text.Range, private val index: Index)
    7.21 +  {
    7.22 +    override def hashCode: Int = (range, index).hashCode
    7.23 +    override def equals(that: Any): Boolean =
    7.24 +      that match {
    7.25 +        case other: Text_Chunk =>
    7.26 +          range == other.range &&
    7.27 +          index == other.index
    7.28 +        case _ => false
    7.29 +      }
    7.30 +
    7.31 +    def decode(symbol_offset: Offset): Text.Offset = index.decode(symbol_offset)
    7.32 +    def decode(symbol_range: Range): Text.Range = index.decode(symbol_range)
    7.33 +    def incorporate(symbol_range: Range): Option[Text.Range] =
    7.34 +    {
    7.35 +      def in(r: Range): Option[Text.Range] =
    7.36 +        range.try_restrict(decode(r)) match {
    7.37 +          case Some(r1) if !r1.is_singularity => Some(r1)
    7.38 +          case _ => None
    7.39 +        }
    7.40 +     in(symbol_range) orElse in(symbol_range - 1)
    7.41 +    }
    7.42 +  }
    7.43 +
    7.44 +
    7.45    /* recoding text */
    7.46  
    7.47    private class Recoder(list: List[(String, String)])
     8.1 --- a/src/Pure/General/word.scala	Sat Apr 26 14:53:22 2014 +0200
     8.2 +++ b/src/Pure/General/word.scala	Sat Apr 26 22:57:51 2014 +0200
     8.3 @@ -2,7 +2,7 @@
     8.4      Module:     PIDE
     8.5      Author:     Makarius
     8.6  
     8.7 -Support for plain text words.
     8.8 +Support for words within Unicode text.
     8.9  */
    8.10  
    8.11  package isabelle
    8.12 @@ -85,6 +85,6 @@
    8.13      explode(_ == sep, text)
    8.14  
    8.15    def explode(text: String): List[String] =
    8.16 -    explode(Symbol.is_ascii_blank(_), text)
    8.17 +    explode(Character.isWhitespace(_), text)
    8.18  }
    8.19  
     9.1 --- a/src/Pure/PIDE/command.scala	Sat Apr 26 14:53:22 2014 +0200
     9.2 +++ b/src/Pure/PIDE/command.scala	Sat Apr 26 22:57:51 2014 +0200
     9.3 @@ -15,7 +15,7 @@
     9.4  object Command
     9.5  {
     9.6    type Edit = (Option[Command], Option[Command])
     9.7 -  type Blob = Exn.Result[(Document.Node.Name, Option[(SHA1.Digest, Text.Chunk)])]
     9.8 +  type Blob = Exn.Result[(Document.Node.Name, Option[(SHA1.Digest, Symbol.Text_Chunk)])]
     9.9  
    9.10  
    9.11  
    9.12 @@ -60,10 +60,10 @@
    9.13  
    9.14    object Markup_Index
    9.15    {
    9.16 -    val markup: Markup_Index = Markup_Index(false, Text.Chunk.Default)
    9.17 +    val markup: Markup_Index = Markup_Index(false, Symbol.Text_Chunk.Default)
    9.18    }
    9.19  
    9.20 -  sealed case class Markup_Index(status: Boolean, chunk_name: Text.Chunk.Name)
    9.21 +  sealed case class Markup_Index(status: Boolean, chunk_name: Symbol.Text_Chunk.Name)
    9.22  
    9.23    object Markups
    9.24    {
    9.25 @@ -84,16 +84,16 @@
    9.26        new Markups(rep + (index -> (this(index) + markup)))
    9.27  
    9.28      def redirection_iterator: Iterator[Document_ID.Generic] =
    9.29 -      for (Markup_Index(_, Text.Chunk.Id(id)) <- rep.keysIterator)
    9.30 +      for (Markup_Index(_, Symbol.Text_Chunk.Id(id)) <- rep.keysIterator)
    9.31          yield id
    9.32  
    9.33      def redirect(other_id: Document_ID.Generic): Markups =
    9.34      {
    9.35        val rep1 =
    9.36          (for {
    9.37 -          (Markup_Index(status, Text.Chunk.Id(id)), markup) <- rep.iterator
    9.38 +          (Markup_Index(status, Symbol.Text_Chunk.Id(id)), markup) <- rep.iterator
    9.39            if other_id == id
    9.40 -        } yield (Markup_Index(status, Text.Chunk.Default), markup)).toMap
    9.41 +        } yield (Markup_Index(status, Symbol.Text_Chunk.Default), markup)).toMap
    9.42        if (rep1.isEmpty) Markups.empty else new Markups(rep1)
    9.43      }
    9.44  
    9.45 @@ -115,7 +115,7 @@
    9.46        Results.merge(states.map(_.results))
    9.47  
    9.48      def merge_markup(states: List[State], index: Markup_Index,
    9.49 -        range: Text.Range, elements: Document.Elements): Markup_Tree =
    9.50 +        range: Text.Range, elements: Markup.Elements): Markup_Tree =
    9.51        Markup_Tree.merge(states.map(_.markup(index)), range, elements)
    9.52    }
    9.53  
    9.54 @@ -156,7 +156,8 @@
    9.55      private def add_status(st: Markup): State =
    9.56        copy(status = st :: status)
    9.57  
    9.58 -    private def add_markup(status: Boolean, chunk_name: Text.Chunk.Name, m: Text.Markup): State =
    9.59 +    private def add_markup(
    9.60 +      status: Boolean, chunk_name: Symbol.Text_Chunk.Name, m: Text.Markup): State =
    9.61      {
    9.62        val markups1 =
    9.63          if (status || Protocol.liberal_status_elements(m.info.name))
    9.64 @@ -167,7 +168,7 @@
    9.65  
    9.66      def accumulate(
    9.67          self_id: Document_ID.Generic => Boolean,
    9.68 -        other_id: Document_ID.Generic => Option[(Text.Chunk.Id, Text.Chunk)],
    9.69 +        other_id: Document_ID.Generic => Option[(Symbol.Text_Chunk.Id, Symbol.Text_Chunk)],
    9.70          message: XML.Elem): State =
    9.71        message match {
    9.72          case XML.Elem(Markup(Markup.STATUS, _), msgs) =>
    9.73 @@ -176,7 +177,7 @@
    9.74                case elem @ XML.Elem(markup, Nil) =>
    9.75                  state.
    9.76                    add_status(markup).
    9.77 -                  add_markup(true, Text.Chunk.Default, Text.Info(command.proper_range, elem))
    9.78 +                  add_markup(true, Symbol.Text_Chunk.Default, Text.Info(command.proper_range, elem))
    9.79                case _ =>
    9.80                  System.err.println("Ignored status message: " + msg)
    9.81                  state
    9.82 @@ -194,7 +195,7 @@
    9.83                    val target =
    9.84                      if (self_id(id) && command.chunks.isDefinedAt(chunk_name))
    9.85                        Some((chunk_name, command.chunks(chunk_name)))
    9.86 -                    else if (chunk_name == Text.Chunk.Default) other_id(id)
    9.87 +                    else if (chunk_name == Symbol.Text_Chunk.Default) other_id(id)
    9.88                      else None
    9.89  
    9.90                    target match {
    9.91 @@ -216,7 +217,7 @@
    9.92                    val range = command.proper_range
    9.93                    val props = Position.purge(atts)
    9.94                    val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args))
    9.95 -                  state.add_markup(false, Text.Chunk.Default, info)
    9.96 +                  state.add_markup(false, Symbol.Text_Chunk.Default, info)
    9.97  
    9.98                  case _ => bad(); state
    9.99                }
   9.100 @@ -365,12 +366,12 @@
   9.101  
   9.102    /* source chunks */
   9.103  
   9.104 -  val chunk: Text.Chunk = Text.Chunk(source)
   9.105 +  val chunk: Symbol.Text_Chunk = Symbol.Text_Chunk(source)
   9.106  
   9.107 -  val chunks: Map[Text.Chunk.Name, Text.Chunk] =
   9.108 -    ((Text.Chunk.Default -> chunk) ::
   9.109 +  val chunks: Map[Symbol.Text_Chunk.Name, Symbol.Text_Chunk] =
   9.110 +    ((Symbol.Text_Chunk.Default -> chunk) ::
   9.111        (for (Exn.Res((name, Some((_, file)))) <- blobs)
   9.112 -        yield (Text.Chunk.File(name.node) -> file))).toMap
   9.113 +        yield (Symbol.Text_Chunk.File(name.node) -> file))).toMap
   9.114  
   9.115    def length: Int = source.length
   9.116    def range: Text.Range = chunk.range
    10.1 --- a/src/Pure/PIDE/document.scala	Sat Apr 26 14:53:22 2014 +0200
    10.2 +++ b/src/Pure/PIDE/document.scala	Sat Apr 26 22:57:51 2014 +0200
    10.3 @@ -45,7 +45,7 @@
    10.4  
    10.5    /* document blobs: auxiliary files */
    10.6  
    10.7 -  sealed case class Blob(bytes: Bytes, chunk: Text.Chunk, changed: Boolean)
    10.8 +  sealed case class Blob(bytes: Bytes, chunk: Symbol.Text_Chunk, changed: Boolean)
    10.9    {
   10.10      def unchanged: Blob = copy(changed = false)
   10.11    }
   10.12 @@ -379,31 +379,6 @@
   10.13    }
   10.14  
   10.15  
   10.16 -  /* markup elements */
   10.17 -
   10.18 -  object Elements
   10.19 -  {
   10.20 -    def apply(elems: Set[String]): Elements = new Elements(elems)
   10.21 -    def apply(elems: String*): Elements = apply(Set(elems: _*))
   10.22 -    val empty: Elements = apply()
   10.23 -    val full: Elements = new Full_Elements
   10.24 -  }
   10.25 -
   10.26 -  sealed class Elements private[Document](private val rep: Set[String])
   10.27 -  {
   10.28 -    def apply(elem: String): Boolean = rep.contains(elem)
   10.29 -    def + (elem: String): Elements = new Elements(rep + elem)
   10.30 -    def ++ (elems: Elements): Elements = new Elements(rep ++ elems.rep)
   10.31 -    override def toString: String = rep.mkString("Elements(", ",", ")")
   10.32 -  }
   10.33 -
   10.34 -  private class Full_Elements extends Elements(Set.empty)
   10.35 -  {
   10.36 -    override def apply(elem: String): Boolean = true
   10.37 -    override def toString: String = "Full_Elements()"
   10.38 -  }
   10.39 -
   10.40 -
   10.41    /* snapshot */
   10.42  
   10.43    object Snapshot
   10.44 @@ -431,13 +406,13 @@
   10.45      def cumulate[A](
   10.46        range: Text.Range,
   10.47        info: A,
   10.48 -      elements: Elements,
   10.49 +      elements: Markup.Elements,
   10.50        result: List[Command.State] => (A, Text.Markup) => Option[A],
   10.51        status: Boolean = false): List[Text.Info[A]]
   10.52  
   10.53      def select[A](
   10.54        range: Text.Range,
   10.55 -      elements: Elements,
   10.56 +      elements: Markup.Elements,
   10.57        result: List[Command.State] => Text.Markup => Option[A],
   10.58        status: Boolean = false): List[Text.Info[A]]
   10.59    }
   10.60 @@ -536,10 +511,11 @@
   10.61        id == st.command.id ||
   10.62        (execs.get(id) match { case Some(st1) => st1.command.id == st.command.id case None => false })
   10.63  
   10.64 -    private def other_id(id: Document_ID.Generic): Option[(Text.Chunk.Id, Text.Chunk)] = None
   10.65 +    private def other_id(id: Document_ID.Generic)
   10.66 +      : Option[(Symbol.Text_Chunk.Id, Symbol.Text_Chunk)] = None
   10.67      /* FIXME
   10.68        (execs.get(id) orElse commands.get(id)).map(st =>
   10.69 -        ((Text.Chunk.Id(st.command.id), st.command.chunk)))
   10.70 +        ((Symbol.Text_Chunk.Id(st.command.id), st.command.chunk)))
   10.71      */
   10.72  
   10.73      private def redirection(st: Command.State): Graph[Document_ID.Command, Unit] =
   10.74 @@ -697,10 +673,10 @@
   10.75        Command.State.merge_results(command_states(version, command))
   10.76  
   10.77      def command_markup(version: Version, command: Command, index: Command.Markup_Index,
   10.78 -        range: Text.Range, elements: Elements): Markup_Tree =
   10.79 +        range: Text.Range, elements: Markup.Elements): Markup_Tree =
   10.80        Command.State.merge_markup(command_states(version, command), index, range, elements)
   10.81  
   10.82 -    def markup_to_XML(version: Version, node: Node, elements: Elements): XML.Body =
   10.83 +    def markup_to_XML(version: Version, node: Node, elements: Markup.Elements): XML.Body =
   10.84        (for {
   10.85          command <- node.commands.iterator
   10.86          markup =
   10.87 @@ -769,15 +745,15 @@
   10.88          def cumulate[A](
   10.89            range: Text.Range,
   10.90            info: A,
   10.91 -          elements: Elements,
   10.92 +          elements: Markup.Elements,
   10.93            result: List[Command.State] => (A, Text.Markup) => Option[A],
   10.94            status: Boolean = false): List[Text.Info[A]] =
   10.95          {
   10.96            val former_range = revert(range).inflate_singularity
   10.97            val (chunk_name, command_iterator) =
   10.98              load_commands match {
   10.99 -              case command :: _ => (Text.Chunk.File(node_name.node), Iterator((command, 0)))
  10.100 -              case _ => (Text.Chunk.Default, node.command_iterator(former_range))
  10.101 +              case command :: _ => (Symbol.Text_Chunk.File(node_name.node), Iterator((command, 0)))
  10.102 +              case _ => (Symbol.Text_Chunk.Default, node.command_iterator(former_range))
  10.103              }
  10.104            val markup_index = Command.Markup_Index(status, chunk_name)
  10.105            (for {
  10.106 @@ -797,7 +773,7 @@
  10.107  
  10.108          def select[A](
  10.109            range: Text.Range,
  10.110 -          elements: Elements,
  10.111 +          elements: Markup.Elements,
  10.112            result: List[Command.State] => Text.Markup => Option[A],
  10.113            status: Boolean = false): List[Text.Info[A]] =
  10.114          {
    11.1 --- a/src/Pure/PIDE/document_id.scala	Sat Apr 26 14:53:22 2014 +0200
    11.2 +++ b/src/Pure/PIDE/document_id.scala	Sat Apr 26 22:57:51 2014 +0200
    11.3 @@ -1,4 +1,5 @@
    11.4  /*  Title:      Pure/PIDE/document_id.scala
    11.5 +    Module:     PIDE
    11.6      Author:     Makarius
    11.7  
    11.8  Unique identifiers for document structure.
    12.1 --- a/src/Pure/PIDE/markup.ML	Sat Apr 26 14:53:22 2014 +0200
    12.2 +++ b/src/Pure/PIDE/markup.ML	Sat Apr 26 22:57:51 2014 +0200
    12.3 @@ -1,7 +1,7 @@
    12.4  (*  Title:      Pure/PIDE/markup.ML
    12.5      Author:     Makarius
    12.6  
    12.7 -Isabelle-specific implementation of quasi-abstract markup elements.
    12.8 +Quasi-abstract markup elements.
    12.9  *)
   12.10  
   12.11  signature MARKUP =
    13.1 --- a/src/Pure/PIDE/markup.scala	Sat Apr 26 14:53:22 2014 +0200
    13.2 +++ b/src/Pure/PIDE/markup.scala	Sat Apr 26 22:57:51 2014 +0200
    13.3 @@ -2,7 +2,7 @@
    13.4      Module:     PIDE
    13.5      Author:     Makarius
    13.6  
    13.7 -Isabelle-specific implementation of quasi-abstract markup elements.
    13.8 +Quasi-abstract markup elements.
    13.9  */
   13.10  
   13.11  package isabelle
   13.12 @@ -10,6 +10,30 @@
   13.13  
   13.14  object Markup
   13.15  {
   13.16 +  /* elements */
   13.17 +
   13.18 +  object Elements
   13.19 +  {
   13.20 +    def apply(elems: Set[String]): Elements = new Elements(elems)
   13.21 +    def apply(elems: String*): Elements = apply(Set(elems: _*))
   13.22 +    val empty: Elements = apply()
   13.23 +    val full: Elements =
   13.24 +      new Elements(Set.empty)
   13.25 +      {
   13.26 +        override def apply(elem: String): Boolean = true
   13.27 +        override def toString: String = "Elements.full"
   13.28 +      }
   13.29 +  }
   13.30 +
   13.31 +  sealed class Elements private[Markup](private val rep: Set[String])
   13.32 +  {
   13.33 +    def apply(elem: String): Boolean = rep.contains(elem)
   13.34 +    def + (elem: String): Elements = new Elements(rep + elem)
   13.35 +    def ++ (elems: Elements): Elements = new Elements(rep ++ elems.rep)
   13.36 +    override def toString: String = rep.mkString("Elements(", ",", ")")
   13.37 +  }
   13.38 +
   13.39 +
   13.40    /* properties */
   13.41  
   13.42    val NAME = "name"
    14.1 --- a/src/Pure/PIDE/markup_tree.scala	Sat Apr 26 14:53:22 2014 +0200
    14.2 +++ b/src/Pure/PIDE/markup_tree.scala	Sat Apr 26 22:57:51 2014 +0200
    14.3 @@ -20,7 +20,7 @@
    14.4  
    14.5    val empty: Markup_Tree = new Markup_Tree(Branches.empty)
    14.6  
    14.7 -  def merge(trees: List[Markup_Tree], range: Text.Range, elements: Document.Elements): Markup_Tree =
    14.8 +  def merge(trees: List[Markup_Tree], range: Text.Range, elements: Markup.Elements): Markup_Tree =
    14.9      (empty /: trees)(_.merge(_, range, elements))
   14.10  
   14.11    def merge_disjoint(trees: List[Markup_Tree]): Markup_Tree =
   14.12 @@ -54,7 +54,7 @@
   14.13    {
   14.14      def markup: List[XML.Elem] = rev_markup.reverse
   14.15  
   14.16 -    def filter_markup(elements: Document.Elements): List[XML.Elem] =
   14.17 +    def filter_markup(elements: Markup.Elements): List[XML.Elem] =
   14.18      {
   14.19        var result: List[XML.Elem] = Nil
   14.20        for { elem <- rev_markup; if (elements(elem.name)) }
   14.21 @@ -161,7 +161,7 @@
   14.22      }
   14.23    }
   14.24  
   14.25 -  def merge(other: Markup_Tree, root_range: Text.Range, elements: Document.Elements): Markup_Tree =
   14.26 +  def merge(other: Markup_Tree, root_range: Text.Range, elements: Markup.Elements): Markup_Tree =
   14.27    {
   14.28      def merge_trees(tree1: Markup_Tree, tree2: Markup_Tree): Markup_Tree =
   14.29        (tree1 /: tree2.branches)(
   14.30 @@ -181,7 +181,7 @@
   14.31      }
   14.32    }
   14.33  
   14.34 -  def cumulate[A](root_range: Text.Range, root_info: A, elements: Document.Elements,
   14.35 +  def cumulate[A](root_range: Text.Range, root_info: A, elements: Markup.Elements,
   14.36      result: (A, Text.Markup) => Option[A]): List[Text.Info[A]] =
   14.37    {
   14.38      def results(x: A, entry: Entry): Option[A] =
   14.39 @@ -230,7 +230,7 @@
   14.40        List((Text.Info(root_range, root_info), overlapping(root_range).toList)))
   14.41    }
   14.42  
   14.43 -  def to_XML(root_range: Text.Range, text: CharSequence, elements: Document.Elements): XML.Body =
   14.44 +  def to_XML(root_range: Text.Range, text: CharSequence, elements: Markup.Elements): XML.Body =
   14.45    {
   14.46      def make_text(start: Text.Offset, stop: Text.Offset): XML.Body =
   14.47        if (start == stop) Nil
    15.1 --- a/src/Pure/PIDE/protocol.scala	Sat Apr 26 14:53:22 2014 +0200
    15.2 +++ b/src/Pure/PIDE/protocol.scala	Sat Apr 26 22:57:51 2014 +0200
    15.3 @@ -101,7 +101,7 @@
    15.4    }
    15.5  
    15.6    val proper_status_elements =
    15.7 -    Document.Elements(Markup.ACCEPTED, Markup.FORKED, Markup.JOINED, Markup.RUNNING,
    15.8 +    Markup.Elements(Markup.ACCEPTED, Markup.FORKED, Markup.JOINED, Markup.RUNNING,
    15.9        Markup.FINISHED, Markup.FAILED)
   15.10  
   15.11    val liberal_status_elements =
   15.12 @@ -187,7 +187,7 @@
   15.13    /* result messages */
   15.14  
   15.15    private val clean_elements =
   15.16 -    Document.Elements(Markup.REPORT, Markup.NO_REPORT)
   15.17 +    Markup.Elements(Markup.REPORT, Markup.NO_REPORT)
   15.18  
   15.19    def clean_message(body: XML.Body): XML.Body =
   15.20      body filter {
   15.21 @@ -308,12 +308,12 @@
   15.22    /* reported positions */
   15.23  
   15.24    private val position_elements =
   15.25 -    Document.Elements(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
   15.26 +    Markup.Elements(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
   15.27  
   15.28    def message_positions(
   15.29      self_id: Document_ID.Generic => Boolean,
   15.30 -    chunk_name: Text.Chunk.Name,
   15.31 -    chunk: Text.Chunk,
   15.32 +    chunk_name: Symbol.Text_Chunk.Name,
   15.33 +    chunk: Symbol.Text_Chunk,
   15.34      message: XML.Elem): Set[Text.Range] =
   15.35    {
   15.36      def elem_positions(props: Properties.T, set: Set[Text.Range]): Set[Text.Range] =
    16.1 --- a/src/Pure/PIDE/text.scala	Sat Apr 26 14:53:22 2014 +0200
    16.2 +++ b/src/Pure/PIDE/text.scala	Sat Apr 26 22:57:51 2014 +0200
    16.3 @@ -72,44 +72,6 @@
    16.4    }
    16.5  
    16.6  
    16.7 -  /* named chunks with sparse symbol index */
    16.8 -
    16.9 -  object Chunk
   16.10 -  {
   16.11 -    sealed abstract class Name
   16.12 -    case object Default extends Name
   16.13 -    case class Id(id: Document_ID.Generic) extends Name
   16.14 -    case class File(name: String) extends Name
   16.15 -
   16.16 -    def apply(text: CharSequence): Chunk =
   16.17 -      new Chunk(Range(0, text.length), Symbol.Index(text))
   16.18 -  }
   16.19 -
   16.20 -  final class Chunk private(val range: Range, private val symbol_index: Symbol.Index)
   16.21 -  {
   16.22 -    override def hashCode: Int = (range, symbol_index).hashCode
   16.23 -    override def equals(that: Any): Boolean =
   16.24 -      that match {
   16.25 -        case other: Chunk =>
   16.26 -          range == other.range &&
   16.27 -          symbol_index == other.symbol_index
   16.28 -        case _ => false
   16.29 -      }
   16.30 -
   16.31 -    def decode(symbol_offset: Symbol.Offset): Offset = symbol_index.decode(symbol_offset)
   16.32 -    def decode(symbol_range: Symbol.Range): Range = symbol_index.decode(symbol_range)
   16.33 -    def incorporate(symbol_range: Symbol.Range): Option[Range] =
   16.34 -    {
   16.35 -      def in(r: Symbol.Range): Option[Range] =
   16.36 -        range.try_restrict(decode(r)) match {
   16.37 -          case Some(r1) if !r1.is_singularity => Some(r1)
   16.38 -          case _ => None
   16.39 -        }
   16.40 -     in(symbol_range) orElse in(symbol_range - 1)
   16.41 -    }
   16.42 -  }
   16.43 -
   16.44 -
   16.45    /* perspective */
   16.46  
   16.47    object Perspective
    17.1 --- a/src/Pure/Thy/html.scala	Sat Apr 26 14:53:22 2014 +0200
    17.2 +++ b/src/Pure/Thy/html.scala	Sat Apr 26 22:57:51 2014 +0200
    17.3 @@ -1,5 +1,5 @@
    17.4  /*  Title:      Pure/Thy/html.scala
    17.5 -    Module:     PIDE-GUI
    17.6 +    Module:     PIDE
    17.7      Author:     Makarius
    17.8  
    17.9  HTML presentation elements.
   17.10 @@ -8,9 +8,6 @@
   17.11  package isabelle
   17.12  
   17.13  
   17.14 -import scala.collection.mutable.ListBuffer
   17.15 -
   17.16 -
   17.17  object HTML
   17.18  {
   17.19    /* encode text */
    18.1 --- a/src/Pure/Tools/find_consts.ML	Sat Apr 26 14:53:22 2014 +0200
    18.2 +++ b/src/Pure/Tools/find_consts.ML	Sat Apr 26 22:57:51 2014 +0200
    18.3 @@ -11,6 +11,7 @@
    18.4        Strict of string
    18.5      | Loose of string
    18.6      | Name of string
    18.7 +  val read_query: Position.T -> string -> (bool * criterion) list
    18.8    val find_consts : Proof.context -> (bool * criterion) list -> unit
    18.9  end;
   18.10  
   18.11 @@ -69,7 +70,7 @@
   18.12  
   18.13  (* find_consts *)
   18.14  
   18.15 -fun find_consts ctxt raw_criteria =
   18.16 +fun pretty_consts ctxt raw_criteria =
   18.17    let
   18.18      val thy = Proof_Context.theory_of ctxt;
   18.19      val low_ranking = 10000;
   18.20 @@ -119,8 +120,10 @@
   18.21        then "nothing found"
   18.22        else "found " ^ string_of_int (length matches) ^ " constant(s):") ::
   18.23      Pretty.str "" ::
   18.24 -    map (pretty_const ctxt) matches
   18.25 -  end |> Pretty.fbreaks |> curry Pretty.blk 0 |> Pretty.writeln;
   18.26 +    map (Pretty.item o single o pretty_const ctxt) matches
   18.27 +  end |> Pretty.fbreaks |> curry Pretty.blk 0;
   18.28 +
   18.29 +fun find_consts ctxt args = Pretty.writeln (pretty_consts ctxt args);
   18.30  
   18.31  
   18.32  (* command syntax *)
   18.33 @@ -132,15 +135,37 @@
   18.34    Parse.reserved "name" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Name ||
   18.35    Parse.xname >> Loose;
   18.36  
   18.37 +val query = Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion);
   18.38 +
   18.39  in
   18.40  
   18.41 +fun read_query pos str =
   18.42 +  Outer_Syntax.scan pos str
   18.43 +  |> filter Token.is_proper
   18.44 +  |> Scan.error (Scan.finite Token.stopper (Parse.!!! (query --| Scan.ahead Parse.eof)))
   18.45 +  |> #1;
   18.46 +
   18.47  val _ =
   18.48    Outer_Syntax.improper_command @{command_spec "find_consts"}
   18.49 -    "find constants by name/type patterns"
   18.50 -    (Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion)
   18.51 -      >> (fn spec => Toplevel.keep (fn state => find_consts (Toplevel.context_of state) spec)));
   18.52 +    "find constants by name / type patterns"
   18.53 +    (query >> (fn spec =>
   18.54 +      Toplevel.keep (fn st =>
   18.55 +        Pretty.writeln (pretty_consts (Toplevel.context_of st) spec))));
   18.56  
   18.57  end;
   18.58  
   18.59 +
   18.60 +(* PIDE query operation *)
   18.61 +
   18.62 +val _ =
   18.63 +  Query_Operation.register "find_consts" (fn {state, args, output_result} =>
   18.64 +    (case try Toplevel.context_of state of
   18.65 +      SOME ctxt =>
   18.66 +        let
   18.67 +          val [query_arg] = args;
   18.68 +          val query = read_query Position.none query_arg;
   18.69 +        in output_result (Pretty.string_of (pretty_consts ctxt query)) end
   18.70 +    | NONE => error "Unknown context"));
   18.71 +
   18.72  end;
   18.73  
    19.1 --- a/src/Tools/jEdit/src/document_model.scala	Sat Apr 26 14:53:22 2014 +0200
    19.2 +++ b/src/Tools/jEdit/src/document_model.scala	Sat Apr 26 22:57:51 2014 +0200
    19.3 @@ -138,7 +138,7 @@
    19.4  
    19.5    /* blob */
    19.6  
    19.7 -  private var _blob: Option[(Bytes, Text.Chunk)] = None  // owned by Swing thread
    19.8 +  private var _blob: Option[(Bytes, Symbol.Text_Chunk)] = None  // owned by Swing thread
    19.9  
   19.10    private def reset_blob(): Unit = Swing_Thread.require { _blob = None }
   19.11  
   19.12 @@ -151,7 +151,7 @@
   19.13              case Some(x) => x
   19.14              case None =>
   19.15                val bytes = PIDE.resources.file_content(buffer)
   19.16 -              val chunk = Text.Chunk(buffer.getSegment(0, buffer.getLength))
   19.17 +              val chunk = Symbol.Text_Chunk(buffer.getSegment(0, buffer.getLength))
   19.18                _blob = Some((bytes, chunk))
   19.19                (bytes, chunk)
   19.20            }
    20.1 --- a/src/Tools/jEdit/src/find_dockable.scala	Sat Apr 26 14:53:22 2014 +0200
    20.2 +++ b/src/Tools/jEdit/src/find_dockable.scala	Sat Apr 26 22:57:51 2014 +0200
    20.3 @@ -9,26 +9,59 @@
    20.4  
    20.5  import isabelle._
    20.6  
    20.7 -import scala.swing.{Button, Component, TextField, CheckBox, Label, ComboBox}
    20.8 -import scala.swing.event.ButtonClicked
    20.9 +import java.awt.event.{ComponentEvent, ComponentAdapter, KeyEvent}
   20.10 +import javax.swing.{JComponent, JTextField}
   20.11  
   20.12 -import java.awt.BorderLayout
   20.13 -import java.awt.event.{ComponentEvent, ComponentAdapter, KeyEvent}
   20.14 +import scala.swing.{Button, Component, TextField, CheckBox, Label,
   20.15 +  ComboBox, TabbedPane, BorderPanel}
   20.16 +import scala.swing.event.{SelectionChanged, ButtonClicked, Key, KeyPressed}
   20.17  
   20.18  import org.gjt.sp.jedit.View
   20.19  
   20.20  
   20.21 +object Find_Dockable
   20.22 +{
   20.23 +  private abstract class Operation(view: View)
   20.24 +  {
   20.25 +    val pretty_text_area = new Pretty_Text_Area(view)
   20.26 +    def query_operation: Query_Operation[View]
   20.27 +    def query: JComponent
   20.28 +    def select: Unit
   20.29 +    def page: TabbedPane.Page
   20.30 +  }
   20.31 +}
   20.32 +
   20.33  class Find_Dockable(view: View, position: String) extends Dockable(view, position)
   20.34  {
   20.35 -  val pretty_text_area = new Pretty_Text_Area(view)
   20.36 -  set_content(pretty_text_area)
   20.37 +  /* common GUI components */
   20.38 +
   20.39 +  private var zoom_factor = 100
   20.40 +
   20.41 +  private val zoom =
   20.42 +    new GUI.Zoom_Box(factor => if (zoom_factor != factor) { zoom_factor = factor; handle_resize() })
   20.43 +    {
   20.44 +      tooltip = "Zoom factor for output font size"
   20.45 +    }
   20.46  
   20.47  
   20.48 -  /* query operation */
   20.49 +  private def make_query(property: String, tooltip: String, apply_query: () => Unit): JTextField =
   20.50 +    new Completion_Popup.History_Text_Field(property)
   20.51 +    {
   20.52 +      override def processKeyEvent(evt: KeyEvent)
   20.53 +      {
   20.54 +        if (evt.getID == KeyEvent.KEY_PRESSED && evt.getKeyCode == KeyEvent.VK_ENTER) apply_query()
   20.55 +        super.processKeyEvent(evt)
   20.56 +      }
   20.57 +      { val max = getPreferredSize; max.width = Integer.MAX_VALUE; setMaximumSize(max) }
   20.58 +      setColumns(40)
   20.59 +      setToolTipText(tooltip)
   20.60 +      setFont(GUI.imitate_font(Font_Info.main_family(), getFont, 1.2))
   20.61 +    }
   20.62  
   20.63 -  private val process_indicator = new Process_Indicator
   20.64  
   20.65 -  private def consume_status(status: Query_Operation.Status.Value)
   20.66 +  /* consume status */
   20.67 +
   20.68 +  def consume_status(process_indicator: Process_Indicator, status: Query_Operation.Status.Value)
   20.69    {
   20.70      status match {
   20.71        case Query_Operation.Status.WAITING =>
   20.72 @@ -40,23 +73,152 @@
   20.73      }
   20.74    }
   20.75  
   20.76 -  private val find_theorems =
   20.77 -    new Query_Operation(PIDE.editor, view, "find_theorems", consume_status _,
   20.78 -      (snapshot, results, body) =>
   20.79 -        pretty_text_area.update(snapshot, results, Pretty.separate(body)))
   20.80 +
   20.81 +  /* find theorems */
   20.82 +
   20.83 +  private val find_theorems = new Find_Dockable.Operation(view)
   20.84 +  {
   20.85 +    /* query */
   20.86 +
   20.87 +    private val process_indicator = new Process_Indicator
   20.88 +
   20.89 +    val query_operation =
   20.90 +      new Query_Operation(PIDE.editor, view, "find_theorems",
   20.91 +        consume_status(process_indicator, _),
   20.92 +        (snapshot, results, body) =>
   20.93 +          pretty_text_area.update(snapshot, results, Pretty.separate(body)))
   20.94 +
   20.95 +    private def apply_query()
   20.96 +    {
   20.97 +      query_operation.apply_query(List(limit.text, allow_dups.selected.toString, query.getText))
   20.98 +    }
   20.99 +
  20.100 +    private val query_label = new Label("Search criteria:") {
  20.101 +      tooltip =
  20.102 +        GUI.tooltip_lines(
  20.103 +          "Search criteria for find operation, e.g.\n\"_ = _\" \"op +\" name: Group -name: monoid")
  20.104 +    }
  20.105 +
  20.106 +    val query = make_query("isabelle-find-theorems", query_label.tooltip, apply_query _)
  20.107 +
  20.108 +
  20.109 +    /* GUI page */
  20.110 +
  20.111 +    private val limit = new TextField(PIDE.options.int("find_theorems_limit").toString, 5) {
  20.112 +      tooltip = "Limit of displayed results"
  20.113 +      verifier = (s: String) =>
  20.114 +        s match { case Properties.Value.Int(x) => x >= 0 case _ => false }
  20.115 +      listenTo(keys)
  20.116 +      reactions += { case KeyPressed(_, Key.Enter, 0, _) => apply_query() }
  20.117 +    }
  20.118 +
  20.119 +    private val allow_dups = new CheckBox("Duplicates") {
  20.120 +      tooltip = "Show all versions of matching theorems"
  20.121 +      selected = false
  20.122 +    }
  20.123 +
  20.124 +    private val apply_button = new Button("Apply") {
  20.125 +      tooltip = "Find theorems meeting specified criteria"
  20.126 +      reactions += { case ButtonClicked(_) => apply_query() }
  20.127 +    }
  20.128 +
  20.129 +    private val control_panel =
  20.130 +      new Wrap_Panel(Wrap_Panel.Alignment.Right)(
  20.131 +        query_label, Component.wrap(query), limit, allow_dups,
  20.132 +        process_indicator.component, apply_button)
  20.133 +
  20.134 +    def select { control_panel.contents += zoom }
  20.135 +
  20.136 +    val page =
  20.137 +      new TabbedPane.Page("Theorems", new BorderPanel {
  20.138 +        add(control_panel, BorderPanel.Position.North)
  20.139 +        add(Component.wrap(pretty_text_area), BorderPanel.Position.Center)
  20.140 +      }, apply_button.tooltip)
  20.141 +  }
  20.142 +
  20.143 +
  20.144 +  /* find consts */
  20.145 +
  20.146 +  private val find_consts = new Find_Dockable.Operation(view)
  20.147 +  {
  20.148 +    /* query */
  20.149 +
  20.150 +    private val process_indicator = new Process_Indicator
  20.151 +
  20.152 +    val query_operation =
  20.153 +      new Query_Operation(PIDE.editor, view, "find_consts",
  20.154 +        consume_status(process_indicator, _),
  20.155 +        (snapshot, results, body) =>
  20.156 +          pretty_text_area.update(snapshot, results, Pretty.separate(body)))
  20.157 +
  20.158 +    private def apply_query()
  20.159 +    {
  20.160 +      query_operation.apply_query(List(query.getText))
  20.161 +    }
  20.162 +
  20.163 +    private val query_label = new Label("Search criteria:") {
  20.164 +      tooltip = GUI.tooltip_lines("Name / type patterns for constants")
  20.165 +    }
  20.166 +
  20.167 +    val query = make_query("isabelle-find-consts", query_label.tooltip, apply_query _)
  20.168 +
  20.169 +
  20.170 +    /* GUI page */
  20.171 +
  20.172 +    private val apply_button = new Button("Apply") {
  20.173 +      tooltip = "Find constants by name / type patterns"
  20.174 +      reactions += { case ButtonClicked(_) => apply_query() }
  20.175 +    }
  20.176 +
  20.177 +    private val control_panel =
  20.178 +      new Wrap_Panel(Wrap_Panel.Alignment.Right)(
  20.179 +        query_label, Component.wrap(query), process_indicator.component, apply_button)
  20.180 +
  20.181 +    def select { control_panel.contents += zoom }
  20.182 +
  20.183 +    val page =
  20.184 +      new TabbedPane.Page("Constants", new BorderPanel {
  20.185 +        add(control_panel, BorderPanel.Position.North)
  20.186 +        add(Component.wrap(pretty_text_area), BorderPanel.Position.Center)
  20.187 +      }, apply_button.tooltip)
  20.188 +  }
  20.189 +
  20.190 +
  20.191 +  /* operations */
  20.192 +
  20.193 +  private val operations = List(find_theorems, find_consts)
  20.194 +
  20.195 +  private val operations_pane = new TabbedPane
  20.196 +  {
  20.197 +    pages ++= operations.map(_.page)
  20.198 +    listenTo(selection)
  20.199 +    reactions += { case SelectionChanged(_) => select_operation() }
  20.200 +  }
  20.201 +
  20.202 +  private def get_operation(): Option[Find_Dockable.Operation] =
  20.203 +    try { Some(operations(operations_pane.selection.index)) }
  20.204 +    catch { case _: IndexOutOfBoundsException => None }
  20.205 +
  20.206 +  private def select_operation() {
  20.207 +    for (op <- get_operation()) op.select
  20.208 +    operations_pane.revalidate
  20.209 +  }
  20.210 +
  20.211 +  override def focusOnDefaultComponent { for (op <- get_operation()) op.query.requestFocus }
  20.212 +
  20.213 +  select_operation()
  20.214 +  set_content(operations_pane)
  20.215  
  20.216  
  20.217    /* resize */
  20.218  
  20.219 -  private var zoom_factor = 100
  20.220 -
  20.221 -  private def handle_resize()
  20.222 -  {
  20.223 -    Swing_Thread.require {}
  20.224 -
  20.225 -    pretty_text_area.resize(
  20.226 -      Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom_factor / 100))
  20.227 -  }
  20.228 +  private def handle_resize(): Unit =
  20.229 +    Swing_Thread.require {
  20.230 +      for (op <- operations) {
  20.231 +        op.pretty_text_area.resize(
  20.232 +          Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom_factor / 100))
  20.233 +      }
  20.234 +    }
  20.235  
  20.236    private val delay_resize =
  20.237      Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
  20.238 @@ -77,67 +239,14 @@
  20.239    {
  20.240      PIDE.session.global_options += main
  20.241      handle_resize()
  20.242 -    find_theorems.activate()
  20.243 +    operations.foreach(op => op.query_operation.activate())
  20.244    }
  20.245  
  20.246    override def exit()
  20.247    {
  20.248 -    find_theorems.deactivate()
  20.249 +    operations.foreach(op => op.query_operation.deactivate())
  20.250      PIDE.session.global_options -= main
  20.251      delay_resize.revoke()
  20.252    }
  20.253 -
  20.254 -
  20.255 -  /* controls */
  20.256 -
  20.257 -  private def clicked
  20.258 -  {
  20.259 -    find_theorems.apply_query(List(limit.text, allow_dups.selected.toString, query.getText))
  20.260 -  }
  20.261 -
  20.262 -  private val query_label = new Label("Search criteria:") {
  20.263 -    tooltip =
  20.264 -      GUI.tooltip_lines(
  20.265 -        "Search criteria for find operation, e.g.\n\"_ = _\" \"op +\" name: Group -name: monoid")
  20.266 -  }
  20.267 -
  20.268 -  private val query = new Completion_Popup.History_Text_Field("isabelle-find-theorems") {
  20.269 -    override def processKeyEvent(evt: KeyEvent)
  20.270 -    {
  20.271 -      if (evt.getID == KeyEvent.KEY_PRESSED && evt.getKeyCode == KeyEvent.VK_ENTER) clicked
  20.272 -      super.processKeyEvent(evt)
  20.273 -    }
  20.274 -    { val max = getPreferredSize; max.width = Integer.MAX_VALUE; setMaximumSize(max) }
  20.275 -    setColumns(40)
  20.276 -    setToolTipText(query_label.tooltip)
  20.277 -    setFont(GUI.imitate_font(Font_Info.main_family(), getFont, 1.2))
  20.278 -  }
  20.279 +}
  20.280  
  20.281 -  private val limit = new TextField(PIDE.options.int("find_theorems_limit").toString, 5) {
  20.282 -    tooltip = "Limit of displayed results"
  20.283 -    verifier = (s: String) =>
  20.284 -      s match { case Properties.Value.Int(x) => x >= 0 case _ => false }
  20.285 -  }
  20.286 -
  20.287 -  private val allow_dups = new CheckBox("Duplicates") {
  20.288 -    tooltip = "Show all versions of matching theorems"
  20.289 -    selected = false
  20.290 -  }
  20.291 -
  20.292 -  private val apply_query = new Button("Apply") {
  20.293 -    tooltip = "Find theorems meeting specified criteria"
  20.294 -    reactions += { case ButtonClicked(_) => clicked }
  20.295 -  }
  20.296 -
  20.297 -  private val zoom = new GUI.Zoom_Box(factor => { zoom_factor = factor; handle_resize() }) {
  20.298 -    tooltip = "Zoom factor for output font size"
  20.299 -  }
  20.300 -
  20.301 -  private val controls =
  20.302 -    new Wrap_Panel(Wrap_Panel.Alignment.Right)(
  20.303 -      query_label, Component.wrap(query), limit, allow_dups,
  20.304 -      process_indicator.component, apply_query, zoom)
  20.305 -  add(controls.peer, BorderLayout.NORTH)
  20.306 -
  20.307 -  override def focusOnDefaultComponent { query.requestFocus }
  20.308 -}
    21.1 --- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Sat Apr 26 14:53:22 2014 +0200
    21.2 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Sat Apr 26 22:57:51 2014 +0200
    21.3 @@ -162,7 +162,7 @@
    21.4            val markup =
    21.5              snapshot.state.command_markup(
    21.6                snapshot.version, command, Command.Markup_Index.markup,
    21.7 -                command.range, Document.Elements.full)
    21.8 +                command.range, Markup.Elements.full)
    21.9            Isabelle_Sidekick.swing_markup_tree(markup, root, (info: Text.Info[List[XML.Elem]]) =>
   21.10                {
   21.11                  val range = info.range + command_start
    22.1 --- a/src/Tools/jEdit/src/jedit_options.scala	Sat Apr 26 14:53:22 2014 +0200
    22.2 +++ b/src/Tools/jEdit/src/jedit_options.scala	Sat Apr 26 22:57:51 2014 +0200
    22.3 @@ -93,6 +93,7 @@
    22.4                case _ => true
    22.5              }
    22.6            })
    22.7 +        GUI.plain_focus_traversal(text_area.peer)
    22.8          text_area
    22.9        }
   22.10      component.load()
    23.1 --- a/src/Tools/jEdit/src/rendering.scala	Sat Apr 26 14:53:22 2014 +0200
    23.2 +++ b/src/Tools/jEdit/src/rendering.scala	Sat Apr 26 22:57:51 2014 +0200
    23.3 @@ -129,28 +129,28 @@
    23.4    /* markup elements */
    23.5  
    23.6    private val semantic_completion_elements =
    23.7 -    Document.Elements(Markup.COMPLETION, Markup.NO_COMPLETION)
    23.8 +    Markup.Elements(Markup.COMPLETION, Markup.NO_COMPLETION)
    23.9  
   23.10    private val language_context_elements =
   23.11 -    Document.Elements(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM,
   23.12 +    Markup.Elements(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM,
   23.13        Markup.CARTOUCHE, Markup.COMMENT, Markup.LANGUAGE,
   23.14        Markup.ML_STRING, Markup.ML_COMMENT)
   23.15  
   23.16    private val highlight_elements =
   23.17 -    Document.Elements(Markup.LANGUAGE, Markup.ML_TYPING, Markup.TOKEN_RANGE,
   23.18 +    Markup.Elements(Markup.LANGUAGE, Markup.ML_TYPING, Markup.TOKEN_RANGE,
   23.19        Markup.ENTITY, Markup.PATH, Markup.URL, Markup.SORTING,
   23.20        Markup.TYPING, Markup.FREE, Markup.SKOLEM, Markup.BOUND,
   23.21        Markup.VAR, Markup.TFREE, Markup.TVAR)
   23.22  
   23.23    private val hyperlink_elements =
   23.24 -    Document.Elements(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.URL)
   23.25 +    Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.URL)
   23.26  
   23.27    private val active_elements =
   23.28 -    Document.Elements(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW,
   23.29 +    Markup.Elements(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW,
   23.30        Markup.SENDBACK, Markup.SIMP_TRACE)
   23.31  
   23.32    private val tooltip_message_elements =
   23.33 -    Document.Elements(Markup.WRITELN, Markup.WARNING, Markup.ERROR, Markup.BAD)
   23.34 +    Markup.Elements(Markup.WRITELN, Markup.WARNING, Markup.ERROR, Markup.BAD)
   23.35  
   23.36    private val tooltip_descriptions =
   23.37      Map(
   23.38 @@ -163,23 +163,23 @@
   23.39        Markup.TVAR -> "schematic type variable")
   23.40  
   23.41    private val tooltip_elements =
   23.42 -    Document.Elements(Markup.LANGUAGE, Markup.TIMING, Markup.ENTITY, Markup.SORTING,
   23.43 +    Markup.Elements(Markup.LANGUAGE, Markup.TIMING, Markup.ENTITY, Markup.SORTING,
   23.44        Markup.TYPING, Markup.ML_TYPING, Markup.PATH, Markup.URL) ++
   23.45 -    Document.Elements(tooltip_descriptions.keySet)
   23.46 +    Markup.Elements(tooltip_descriptions.keySet)
   23.47  
   23.48    private val gutter_elements =
   23.49 -    Document.Elements(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
   23.50 +    Markup.Elements(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
   23.51  
   23.52    private val squiggly_elements =
   23.53 -    Document.Elements(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
   23.54 +    Markup.Elements(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
   23.55  
   23.56    private val line_background_elements =
   23.57 -    Document.Elements(Markup.WRITELN_MESSAGE, Markup.TRACING_MESSAGE,
   23.58 +    Markup.Elements(Markup.WRITELN_MESSAGE, Markup.TRACING_MESSAGE,
   23.59        Markup.WARNING_MESSAGE, Markup.ERROR_MESSAGE,
   23.60        Markup.INFORMATION)
   23.61  
   23.62    private val separator_elements =
   23.63 -    Document.Elements(Markup.SEPARATOR)
   23.64 +    Markup.Elements(Markup.SEPARATOR)
   23.65  
   23.66    private val background_elements =
   23.67      Protocol.proper_status_elements + Markup.WRITELN_MESSAGE +
   23.68 @@ -188,14 +188,14 @@
   23.69        active_elements
   23.70  
   23.71    private val foreground_elements =
   23.72 -    Document.Elements(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM,
   23.73 +    Markup.Elements(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM,
   23.74        Markup.CARTOUCHE, Markup.ANTIQUOTED)
   23.75  
   23.76    private val bullet_elements =
   23.77 -    Document.Elements(Markup.BULLET)
   23.78 +    Markup.Elements(Markup.BULLET)
   23.79  
   23.80    private val fold_depth_elements =
   23.81 -    Document.Elements(Markup.TEXT_FOLD, Markup.GOAL, Markup.SUBGOAL)
   23.82 +    Markup.Elements(Markup.TEXT_FOLD, Markup.GOAL, Markup.SUBGOAL)
   23.83  }
   23.84  
   23.85  
   23.86 @@ -287,7 +287,7 @@
   23.87    /* spell checker */
   23.88  
   23.89    private lazy val spell_checker_elements =
   23.90 -    Document.Elements(space_explode(',', options.string("spell_checker_elements")): _*)
   23.91 +    Markup.Elements(space_explode(',', options.string("spell_checker_elements")): _*)
   23.92  
   23.93    def spell_checker_ranges(range: Text.Range): List[Text.Range] =
   23.94      snapshot.select(range, spell_checker_elements, _ => _ => Some(())).map(_.range)
   23.95 @@ -407,7 +407,7 @@
   23.96  
   23.97    def command_results(range: Text.Range): Command.Results =
   23.98      Command.State.merge_results(
   23.99 -      snapshot.select[List[Command.State]](range, Document.Elements.full, command_states =>
  23.100 +      snapshot.select[List[Command.State]](range, Markup.Elements.full, command_states =>
  23.101          { case _ => Some(command_states) }).flatMap(_.info))
  23.102  
  23.103  
  23.104 @@ -695,7 +695,7 @@
  23.105        Markup.SML_COMMENT -> inner_comment_color)
  23.106  
  23.107    private lazy val text_color_elements =
  23.108 -    Document.Elements(text_colors.keySet)
  23.109 +    Markup.Elements(text_colors.keySet)
  23.110  
  23.111    def text_color(range: Text.Range, color: Color): List[Text.Info[Color]] =
  23.112    {
    24.1 --- a/src/Tools/jEdit/src/simplifier_trace_window.scala	Sat Apr 26 14:53:22 2014 +0200
    24.2 +++ b/src/Tools/jEdit/src/simplifier_trace_window.scala	Sat Apr 26 22:57:51 2014 +0200
    24.3 @@ -207,9 +207,7 @@
    24.4    val use_regex = new CheckBox("Regex")
    24.5  
    24.6    private val controls = new Wrap_Panel(Wrap_Panel.Alignment.Right)(
    24.7 -    new Label {
    24.8 -      text = "Search"
    24.9 -    },
   24.10 +    new Label("Search"),
   24.11      new TextField(30) {
   24.12        listenTo(keys)
   24.13        reactions += {
    25.1 --- a/src/Tools/jEdit/src/symbols_dockable.scala	Sat Apr 26 14:53:22 2014 +0200
    25.2 +++ b/src/Tools/jEdit/src/symbols_dockable.scala	Sat Apr 26 22:57:51 2014 +0200
    25.3 @@ -9,9 +9,7 @@
    25.4  
    25.5  import isabelle._
    25.6  
    25.7 -import java.awt.Font
    25.8 -
    25.9 -import scala.swing.event.ValueChanged
   25.10 +import scala.swing.event.{SelectionChanged, ValueChanged}
   25.11  import scala.swing.{Action, Button, TabbedPane, TextField, BorderPanel, Label, ScrollPane}
   25.12  
   25.13  import org.gjt.sp.jedit.View
   25.14 @@ -19,10 +17,6 @@
   25.15  
   25.16  class Symbols_Dockable(view: View, position: String) extends Dockable(view, position)
   25.17  {
   25.18 -  val searchspace =
   25.19 -    for ((group, symbols) <- Symbol.groups; sym <- symbols)
   25.20 -      yield (sym, Word.lowercase(sym))
   25.21 -
   25.22    private class Symbol_Component(val symbol: String) extends Button
   25.23    {
   25.24      private val decoded = Symbol.decode(symbol)
   25.25 @@ -56,39 +50,52 @@
   25.26      tooltip = "Reset control symbols within text"
   25.27    }
   25.28  
   25.29 -  val group_tabs: TabbedPane = new TabbedPane {
   25.30 +  private val group_tabs: TabbedPane = new TabbedPane {
   25.31      pages ++=
   25.32 -      Symbol.groups map { case (group, symbols) =>
   25.33 +      Symbol.groups.map({ case (group, symbols) =>
   25.34          new TabbedPane.Page(group,
   25.35            new ScrollPane(new Wrap_Panel {
   25.36              contents ++= symbols.map(new Symbol_Component(_))
   25.37              if (group == "control") contents += new Reset_Component
   25.38            }), null)
   25.39 -      }
   25.40 -    pages += new TabbedPane.Page("search", new BorderPanel {
   25.41 -      val search = new TextField(10)
   25.42 -      val results_panel = new Wrap_Panel
   25.43 -      add(search, BorderPanel.Position.North)
   25.44 -      add(new ScrollPane(results_panel), BorderPanel.Position.Center)
   25.45 -      listenTo(search)
   25.46 -      val delay_search =
   25.47 -        Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) {
   25.48 -          val max_results = PIDE.options.int("jedit_symbols_search_limit") max 0
   25.49 -          results_panel.contents.clear
   25.50 -          val results =
   25.51 -            (searchspace filter
   25.52 -              (Word.explode(Word.lowercase(search.text)) forall _._2.contains)
   25.53 -              take (max_results + 1)).toList
   25.54 -          for ((sym, _) <- results)
   25.55 -            results_panel.contents += new Symbol_Component(sym)
   25.56 -          if (results.length > max_results) results_panel.contents += new Label("...")
   25.57 -          revalidate
   25.58 -          repaint
   25.59 -        }
   25.60 -      reactions += { case ValueChanged(`search`) => delay_search.invoke() }
   25.61 -    }, "Search Symbols")
   25.62 -    pages.map(p =>
   25.63 -      p.title = Word.implode(Word.explode('_', p.title).map(Word.perhaps_capitalize(_))))
   25.64 +      })
   25.65 +
   25.66 +    val search_field = new TextField(10)
   25.67 +    val search_page =
   25.68 +      new TabbedPane.Page("search", new BorderPanel {
   25.69 +        val results_panel = new Wrap_Panel
   25.70 +        add(search_field, BorderPanel.Position.North)
   25.71 +        add(new ScrollPane(results_panel), BorderPanel.Position.Center)
   25.72 +  
   25.73 +        val search_space =
   25.74 +          (for (sym <- Symbol.names.keysIterator) yield (sym, Word.lowercase(sym))).toList
   25.75 +        val delay_search =
   25.76 +          Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) {
   25.77 +            val search_words = Word.explode(Word.lowercase(search_field.text))
   25.78 +            val search_limit = PIDE.options.int("jedit_symbols_search_limit") max 0
   25.79 +            val results =
   25.80 +              for ((sym, s) <- search_space; if search_words.forall(s.contains(_))) yield sym
   25.81 +
   25.82 +            results_panel.contents.clear
   25.83 +            for (sym <- results.take(search_limit))
   25.84 +              results_panel.contents += new Symbol_Component(sym)
   25.85 +            if (results.length > search_limit)
   25.86 +              results_panel.contents +=
   25.87 +                new Label("...") { tooltip = "(" + (results.length - search_limit) + " more)" }
   25.88 +            revalidate
   25.89 +            repaint
   25.90 +          }
   25.91 +          search_field.reactions += { case ValueChanged(_) => delay_search.invoke() }
   25.92 +      }, "Search Symbols")
   25.93 +    pages += search_page
   25.94 +
   25.95 +    listenTo(selection)
   25.96 +    reactions += {
   25.97 +      case SelectionChanged(_) if selection.page == search_page => search_field.requestFocus
   25.98 +    }
   25.99 +
  25.100 +    for (page <- pages)
  25.101 +      page.title = Word.implode(Word.explode('_', page.title).map(Word.perhaps_capitalize(_)))
  25.102    }
  25.103    set_content(group_tabs)
  25.104  }