--- a/NEWS Sat Apr 26 14:53:22 2014 +0200
+++ b/NEWS Sat Apr 26 22:57:51 2014 +0200
@@ -109,6 +109,9 @@
* Document panel: simplied interaction where every single mouse click
(re)opens document via desktop environment or as jEdit buffer.
+* Find panel: support for 'find_consts' in addition to
+'find_theorems'.
+
* Option "jedit_print_mode" (see also "Plugin Options / Isabelle /
General") allows to specify additional print modes for the prover
process, without requiring old-fashioned command-line invocation of
--- a/src/HOL/Hahn_Banach/Hahn_Banach.thy Sat Apr 26 14:53:22 2014 +0200
+++ b/src/HOL/Hahn_Banach/Hahn_Banach.thy Sat Apr 26 22:57:51 2014 +0200
@@ -391,7 +391,7 @@
ultimately show "0 \<le> p x"
by (simp add: p_def zero_le_mult_iff)
- txt {* @{text p} is absolutely homogenous: *}
+ txt {* @{text p} is absolutely homogeneous: *}
show "p (a \<cdot> x) = \<bar>a\<bar> * p x"
proof -
--- a/src/HOL/Hahn_Banach/Normed_Space.thy Sat Apr 26 14:53:22 2014 +0200
+++ b/src/HOL/Hahn_Banach/Normed_Space.thy Sat Apr 26 22:57:51 2014 +0200
@@ -13,7 +13,7 @@
text {*
A \emph{seminorm} @{text "\<parallel>\<cdot>\<parallel>"} is a function on a real vector space
into the reals that has the following properties: it is positive
- definite, absolute homogenous and subadditive.
+ definite, absolute homogeneous and subadditive.
*}
locale seminorm =
--- a/src/Pure/GUI/gui.scala Sat Apr 26 14:53:22 2014 +0200
+++ b/src/Pure/GUI/gui.scala Sat Apr 26 22:57:51 2014 +0200
@@ -9,10 +9,10 @@
import java.lang.{ClassLoader, ClassNotFoundException, NoSuchMethodException}
-import java.awt.{Image, Component, Container, Toolkit, Window, Font}
+import java.awt.{Image, Component, Container, Toolkit, Window, Font, KeyboardFocusManager}
import java.awt.font.{TextAttribute, TransformAttribute, FontRenderContext, LineMetrics}
import java.awt.geom.AffineTransform
-import javax.swing.{ImageIcon, JOptionPane, UIManager, JLayeredPane, JFrame, JWindow}
+import javax.swing.{ImageIcon, JOptionPane, UIManager, JLayeredPane, JFrame, JWindow, JButton}
import scala.collection.convert.WrapAsJava
import scala.swing.{ComboBox, TextArea, ScrollPane}
@@ -39,6 +39,18 @@
UIManager.getSystemLookAndFeelClassName() == UIManager.getLookAndFeel.getClass.getName
+ /* plain focus traversal, notably for text fields */
+
+ def plain_focus_traversal(component: Component)
+ {
+ val dummy_button = new JButton
+ def apply(id: Int): Unit =
+ component.setFocusTraversalKeys(id, dummy_button.getFocusTraversalKeys(id))
+ apply(KeyboardFocusManager.FORWARD_TRAVERSAL_KEYS)
+ apply(KeyboardFocusManager.BACKWARD_TRAVERSAL_KEYS)
+ }
+
+
/* X11 window manager */
def window_manager(): Option[String] =
--- a/src/Pure/General/multi_map.scala Sat Apr 26 14:53:22 2014 +0200
+++ b/src/Pure/General/multi_map.scala Sat Apr 26 22:57:51 2014 +0200
@@ -1,5 +1,6 @@
/* Title: Pure/General/multi_map.scala
Module: PIDE
+ Author: Makarius
Maps with multiple entries per key.
*/
--- a/src/Pure/General/position.scala Sat Apr 26 14:53:22 2014 +0200
+++ b/src/Pure/General/position.scala Sat Apr 26 22:57:51 2014 +0200
@@ -83,13 +83,13 @@
object Reported
{
- def unapply(pos: T): Option[(Long, Text.Chunk.Name, Symbol.Range)] =
+ def unapply(pos: T): Option[(Long, Symbol.Text_Chunk.Name, Symbol.Range)] =
(pos, pos) match {
case (Id(id), Range(range)) =>
val chunk_name =
pos match {
- case File(name) => Text.Chunk.File(name)
- case _ => Text.Chunk.Default
+ case File(name) => Symbol.Text_Chunk.File(name)
+ case _ => Symbol.Text_Chunk.Default
}
Some((id, chunk_name, range))
case _ => None
--- a/src/Pure/General/symbol.scala Sat Apr 26 14:53:22 2014 +0200
+++ b/src/Pure/General/symbol.scala Sat Apr 26 22:57:51 2014 +0200
@@ -179,6 +179,44 @@
}
+ /* text chunks */
+
+ object Text_Chunk
+ {
+ sealed abstract class Name
+ case object Default extends Name
+ case class Id(id: Document_ID.Generic) extends Name
+ case class File(name: String) extends Name
+
+ def apply(text: CharSequence): Text_Chunk =
+ new Text_Chunk(Text.Range(0, text.length), Index(text))
+ }
+
+ final class Text_Chunk private(val range: Text.Range, private val index: Index)
+ {
+ override def hashCode: Int = (range, index).hashCode
+ override def equals(that: Any): Boolean =
+ that match {
+ case other: Text_Chunk =>
+ range == other.range &&
+ index == other.index
+ case _ => false
+ }
+
+ def decode(symbol_offset: Offset): Text.Offset = index.decode(symbol_offset)
+ def decode(symbol_range: Range): Text.Range = index.decode(symbol_range)
+ def incorporate(symbol_range: Range): Option[Text.Range] =
+ {
+ def in(r: Range): Option[Text.Range] =
+ range.try_restrict(decode(r)) match {
+ case Some(r1) if !r1.is_singularity => Some(r1)
+ case _ => None
+ }
+ in(symbol_range) orElse in(symbol_range - 1)
+ }
+ }
+
+
/* recoding text */
private class Recoder(list: List[(String, String)])
--- a/src/Pure/General/word.scala Sat Apr 26 14:53:22 2014 +0200
+++ b/src/Pure/General/word.scala Sat Apr 26 22:57:51 2014 +0200
@@ -2,7 +2,7 @@
Module: PIDE
Author: Makarius
-Support for plain text words.
+Support for words within Unicode text.
*/
package isabelle
@@ -85,6 +85,6 @@
explode(_ == sep, text)
def explode(text: String): List[String] =
- explode(Symbol.is_ascii_blank(_), text)
+ explode(Character.isWhitespace(_), text)
}
--- a/src/Pure/PIDE/command.scala Sat Apr 26 14:53:22 2014 +0200
+++ b/src/Pure/PIDE/command.scala Sat Apr 26 22:57:51 2014 +0200
@@ -15,7 +15,7 @@
object Command
{
type Edit = (Option[Command], Option[Command])
- type Blob = Exn.Result[(Document.Node.Name, Option[(SHA1.Digest, Text.Chunk)])]
+ type Blob = Exn.Result[(Document.Node.Name, Option[(SHA1.Digest, Symbol.Text_Chunk)])]
@@ -60,10 +60,10 @@
object Markup_Index
{
- val markup: Markup_Index = Markup_Index(false, Text.Chunk.Default)
+ val markup: Markup_Index = Markup_Index(false, Symbol.Text_Chunk.Default)
}
- sealed case class Markup_Index(status: Boolean, chunk_name: Text.Chunk.Name)
+ sealed case class Markup_Index(status: Boolean, chunk_name: Symbol.Text_Chunk.Name)
object Markups
{
@@ -84,16 +84,16 @@
new Markups(rep + (index -> (this(index) + markup)))
def redirection_iterator: Iterator[Document_ID.Generic] =
- for (Markup_Index(_, Text.Chunk.Id(id)) <- rep.keysIterator)
+ for (Markup_Index(_, Symbol.Text_Chunk.Id(id)) <- rep.keysIterator)
yield id
def redirect(other_id: Document_ID.Generic): Markups =
{
val rep1 =
(for {
- (Markup_Index(status, Text.Chunk.Id(id)), markup) <- rep.iterator
+ (Markup_Index(status, Symbol.Text_Chunk.Id(id)), markup) <- rep.iterator
if other_id == id
- } yield (Markup_Index(status, Text.Chunk.Default), markup)).toMap
+ } yield (Markup_Index(status, Symbol.Text_Chunk.Default), markup)).toMap
if (rep1.isEmpty) Markups.empty else new Markups(rep1)
}
@@ -115,7 +115,7 @@
Results.merge(states.map(_.results))
def merge_markup(states: List[State], index: Markup_Index,
- range: Text.Range, elements: Document.Elements): Markup_Tree =
+ range: Text.Range, elements: Markup.Elements): Markup_Tree =
Markup_Tree.merge(states.map(_.markup(index)), range, elements)
}
@@ -156,7 +156,8 @@
private def add_status(st: Markup): State =
copy(status = st :: status)
- private def add_markup(status: Boolean, chunk_name: Text.Chunk.Name, m: Text.Markup): State =
+ private def add_markup(
+ status: Boolean, chunk_name: Symbol.Text_Chunk.Name, m: Text.Markup): State =
{
val markups1 =
if (status || Protocol.liberal_status_elements(m.info.name))
@@ -167,7 +168,7 @@
def accumulate(
self_id: Document_ID.Generic => Boolean,
- other_id: Document_ID.Generic => Option[(Text.Chunk.Id, Text.Chunk)],
+ other_id: Document_ID.Generic => Option[(Symbol.Text_Chunk.Id, Symbol.Text_Chunk)],
message: XML.Elem): State =
message match {
case XML.Elem(Markup(Markup.STATUS, _), msgs) =>
@@ -176,7 +177,7 @@
case elem @ XML.Elem(markup, Nil) =>
state.
add_status(markup).
- add_markup(true, Text.Chunk.Default, Text.Info(command.proper_range, elem))
+ add_markup(true, Symbol.Text_Chunk.Default, Text.Info(command.proper_range, elem))
case _ =>
System.err.println("Ignored status message: " + msg)
state
@@ -194,7 +195,7 @@
val target =
if (self_id(id) && command.chunks.isDefinedAt(chunk_name))
Some((chunk_name, command.chunks(chunk_name)))
- else if (chunk_name == Text.Chunk.Default) other_id(id)
+ else if (chunk_name == Symbol.Text_Chunk.Default) other_id(id)
else None
target match {
@@ -216,7 +217,7 @@
val range = command.proper_range
val props = Position.purge(atts)
val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args))
- state.add_markup(false, Text.Chunk.Default, info)
+ state.add_markup(false, Symbol.Text_Chunk.Default, info)
case _ => bad(); state
}
@@ -365,12 +366,12 @@
/* source chunks */
- val chunk: Text.Chunk = Text.Chunk(source)
+ val chunk: Symbol.Text_Chunk = Symbol.Text_Chunk(source)
- val chunks: Map[Text.Chunk.Name, Text.Chunk] =
- ((Text.Chunk.Default -> chunk) ::
+ val chunks: Map[Symbol.Text_Chunk.Name, Symbol.Text_Chunk] =
+ ((Symbol.Text_Chunk.Default -> chunk) ::
(for (Exn.Res((name, Some((_, file)))) <- blobs)
- yield (Text.Chunk.File(name.node) -> file))).toMap
+ yield (Symbol.Text_Chunk.File(name.node) -> file))).toMap
def length: Int = source.length
def range: Text.Range = chunk.range
--- a/src/Pure/PIDE/document.scala Sat Apr 26 14:53:22 2014 +0200
+++ b/src/Pure/PIDE/document.scala Sat Apr 26 22:57:51 2014 +0200
@@ -45,7 +45,7 @@
/* document blobs: auxiliary files */
- sealed case class Blob(bytes: Bytes, chunk: Text.Chunk, changed: Boolean)
+ sealed case class Blob(bytes: Bytes, chunk: Symbol.Text_Chunk, changed: Boolean)
{
def unchanged: Blob = copy(changed = false)
}
@@ -379,31 +379,6 @@
}
- /* markup elements */
-
- object Elements
- {
- def apply(elems: Set[String]): Elements = new Elements(elems)
- def apply(elems: String*): Elements = apply(Set(elems: _*))
- val empty: Elements = apply()
- val full: Elements = new Full_Elements
- }
-
- sealed class Elements private[Document](private val rep: Set[String])
- {
- def apply(elem: String): Boolean = rep.contains(elem)
- def + (elem: String): Elements = new Elements(rep + elem)
- def ++ (elems: Elements): Elements = new Elements(rep ++ elems.rep)
- override def toString: String = rep.mkString("Elements(", ",", ")")
- }
-
- private class Full_Elements extends Elements(Set.empty)
- {
- override def apply(elem: String): Boolean = true
- override def toString: String = "Full_Elements()"
- }
-
-
/* snapshot */
object Snapshot
@@ -431,13 +406,13 @@
def cumulate[A](
range: Text.Range,
info: A,
- elements: Elements,
+ elements: Markup.Elements,
result: List[Command.State] => (A, Text.Markup) => Option[A],
status: Boolean = false): List[Text.Info[A]]
def select[A](
range: Text.Range,
- elements: Elements,
+ elements: Markup.Elements,
result: List[Command.State] => Text.Markup => Option[A],
status: Boolean = false): List[Text.Info[A]]
}
@@ -536,10 +511,11 @@
id == st.command.id ||
(execs.get(id) match { case Some(st1) => st1.command.id == st.command.id case None => false })
- private def other_id(id: Document_ID.Generic): Option[(Text.Chunk.Id, Text.Chunk)] = None
+ private def other_id(id: Document_ID.Generic)
+ : Option[(Symbol.Text_Chunk.Id, Symbol.Text_Chunk)] = None
/* FIXME
(execs.get(id) orElse commands.get(id)).map(st =>
- ((Text.Chunk.Id(st.command.id), st.command.chunk)))
+ ((Symbol.Text_Chunk.Id(st.command.id), st.command.chunk)))
*/
private def redirection(st: Command.State): Graph[Document_ID.Command, Unit] =
@@ -697,10 +673,10 @@
Command.State.merge_results(command_states(version, command))
def command_markup(version: Version, command: Command, index: Command.Markup_Index,
- range: Text.Range, elements: Elements): Markup_Tree =
+ range: Text.Range, elements: Markup.Elements): Markup_Tree =
Command.State.merge_markup(command_states(version, command), index, range, elements)
- def markup_to_XML(version: Version, node: Node, elements: Elements): XML.Body =
+ def markup_to_XML(version: Version, node: Node, elements: Markup.Elements): XML.Body =
(for {
command <- node.commands.iterator
markup =
@@ -769,15 +745,15 @@
def cumulate[A](
range: Text.Range,
info: A,
- elements: Elements,
+ elements: Markup.Elements,
result: List[Command.State] => (A, Text.Markup) => Option[A],
status: Boolean = false): List[Text.Info[A]] =
{
val former_range = revert(range).inflate_singularity
val (chunk_name, command_iterator) =
load_commands match {
- case command :: _ => (Text.Chunk.File(node_name.node), Iterator((command, 0)))
- case _ => (Text.Chunk.Default, node.command_iterator(former_range))
+ case command :: _ => (Symbol.Text_Chunk.File(node_name.node), Iterator((command, 0)))
+ case _ => (Symbol.Text_Chunk.Default, node.command_iterator(former_range))
}
val markup_index = Command.Markup_Index(status, chunk_name)
(for {
@@ -797,7 +773,7 @@
def select[A](
range: Text.Range,
- elements: Elements,
+ elements: Markup.Elements,
result: List[Command.State] => Text.Markup => Option[A],
status: Boolean = false): List[Text.Info[A]] =
{
--- a/src/Pure/PIDE/document_id.scala Sat Apr 26 14:53:22 2014 +0200
+++ b/src/Pure/PIDE/document_id.scala Sat Apr 26 22:57:51 2014 +0200
@@ -1,4 +1,5 @@
/* Title: Pure/PIDE/document_id.scala
+ Module: PIDE
Author: Makarius
Unique identifiers for document structure.
--- a/src/Pure/PIDE/markup.ML Sat Apr 26 14:53:22 2014 +0200
+++ b/src/Pure/PIDE/markup.ML Sat Apr 26 22:57:51 2014 +0200
@@ -1,7 +1,7 @@
(* Title: Pure/PIDE/markup.ML
Author: Makarius
-Isabelle-specific implementation of quasi-abstract markup elements.
+Quasi-abstract markup elements.
*)
signature MARKUP =
--- a/src/Pure/PIDE/markup.scala Sat Apr 26 14:53:22 2014 +0200
+++ b/src/Pure/PIDE/markup.scala Sat Apr 26 22:57:51 2014 +0200
@@ -2,7 +2,7 @@
Module: PIDE
Author: Makarius
-Isabelle-specific implementation of quasi-abstract markup elements.
+Quasi-abstract markup elements.
*/
package isabelle
@@ -10,6 +10,30 @@
object Markup
{
+ /* elements */
+
+ object Elements
+ {
+ def apply(elems: Set[String]): Elements = new Elements(elems)
+ def apply(elems: String*): Elements = apply(Set(elems: _*))
+ val empty: Elements = apply()
+ val full: Elements =
+ new Elements(Set.empty)
+ {
+ override def apply(elem: String): Boolean = true
+ override def toString: String = "Elements.full"
+ }
+ }
+
+ sealed class Elements private[Markup](private val rep: Set[String])
+ {
+ def apply(elem: String): Boolean = rep.contains(elem)
+ def + (elem: String): Elements = new Elements(rep + elem)
+ def ++ (elems: Elements): Elements = new Elements(rep ++ elems.rep)
+ override def toString: String = rep.mkString("Elements(", ",", ")")
+ }
+
+
/* properties */
val NAME = "name"
--- a/src/Pure/PIDE/markup_tree.scala Sat Apr 26 14:53:22 2014 +0200
+++ b/src/Pure/PIDE/markup_tree.scala Sat Apr 26 22:57:51 2014 +0200
@@ -20,7 +20,7 @@
val empty: Markup_Tree = new Markup_Tree(Branches.empty)
- def merge(trees: List[Markup_Tree], range: Text.Range, elements: Document.Elements): Markup_Tree =
+ def merge(trees: List[Markup_Tree], range: Text.Range, elements: Markup.Elements): Markup_Tree =
(empty /: trees)(_.merge(_, range, elements))
def merge_disjoint(trees: List[Markup_Tree]): Markup_Tree =
@@ -54,7 +54,7 @@
{
def markup: List[XML.Elem] = rev_markup.reverse
- def filter_markup(elements: Document.Elements): List[XML.Elem] =
+ def filter_markup(elements: Markup.Elements): List[XML.Elem] =
{
var result: List[XML.Elem] = Nil
for { elem <- rev_markup; if (elements(elem.name)) }
@@ -161,7 +161,7 @@
}
}
- def merge(other: Markup_Tree, root_range: Text.Range, elements: Document.Elements): Markup_Tree =
+ def merge(other: Markup_Tree, root_range: Text.Range, elements: Markup.Elements): Markup_Tree =
{
def merge_trees(tree1: Markup_Tree, tree2: Markup_Tree): Markup_Tree =
(tree1 /: tree2.branches)(
@@ -181,7 +181,7 @@
}
}
- def cumulate[A](root_range: Text.Range, root_info: A, elements: Document.Elements,
+ def cumulate[A](root_range: Text.Range, root_info: A, elements: Markup.Elements,
result: (A, Text.Markup) => Option[A]): List[Text.Info[A]] =
{
def results(x: A, entry: Entry): Option[A] =
@@ -230,7 +230,7 @@
List((Text.Info(root_range, root_info), overlapping(root_range).toList)))
}
- def to_XML(root_range: Text.Range, text: CharSequence, elements: Document.Elements): XML.Body =
+ def to_XML(root_range: Text.Range, text: CharSequence, elements: Markup.Elements): XML.Body =
{
def make_text(start: Text.Offset, stop: Text.Offset): XML.Body =
if (start == stop) Nil
--- a/src/Pure/PIDE/protocol.scala Sat Apr 26 14:53:22 2014 +0200
+++ b/src/Pure/PIDE/protocol.scala Sat Apr 26 22:57:51 2014 +0200
@@ -101,7 +101,7 @@
}
val proper_status_elements =
- Document.Elements(Markup.ACCEPTED, Markup.FORKED, Markup.JOINED, Markup.RUNNING,
+ Markup.Elements(Markup.ACCEPTED, Markup.FORKED, Markup.JOINED, Markup.RUNNING,
Markup.FINISHED, Markup.FAILED)
val liberal_status_elements =
@@ -187,7 +187,7 @@
/* result messages */
private val clean_elements =
- Document.Elements(Markup.REPORT, Markup.NO_REPORT)
+ Markup.Elements(Markup.REPORT, Markup.NO_REPORT)
def clean_message(body: XML.Body): XML.Body =
body filter {
@@ -308,12 +308,12 @@
/* reported positions */
private val position_elements =
- Document.Elements(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
+ Markup.Elements(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
def message_positions(
self_id: Document_ID.Generic => Boolean,
- chunk_name: Text.Chunk.Name,
- chunk: Text.Chunk,
+ chunk_name: Symbol.Text_Chunk.Name,
+ chunk: Symbol.Text_Chunk,
message: XML.Elem): Set[Text.Range] =
{
def elem_positions(props: Properties.T, set: Set[Text.Range]): Set[Text.Range] =
--- a/src/Pure/PIDE/text.scala Sat Apr 26 14:53:22 2014 +0200
+++ b/src/Pure/PIDE/text.scala Sat Apr 26 22:57:51 2014 +0200
@@ -72,44 +72,6 @@
}
- /* named chunks with sparse symbol index */
-
- object Chunk
- {
- sealed abstract class Name
- case object Default extends Name
- case class Id(id: Document_ID.Generic) extends Name
- case class File(name: String) extends Name
-
- def apply(text: CharSequence): Chunk =
- new Chunk(Range(0, text.length), Symbol.Index(text))
- }
-
- final class Chunk private(val range: Range, private val symbol_index: Symbol.Index)
- {
- override def hashCode: Int = (range, symbol_index).hashCode
- override def equals(that: Any): Boolean =
- that match {
- case other: Chunk =>
- range == other.range &&
- symbol_index == other.symbol_index
- case _ => false
- }
-
- def decode(symbol_offset: Symbol.Offset): Offset = symbol_index.decode(symbol_offset)
- def decode(symbol_range: Symbol.Range): Range = symbol_index.decode(symbol_range)
- def incorporate(symbol_range: Symbol.Range): Option[Range] =
- {
- def in(r: Symbol.Range): Option[Range] =
- range.try_restrict(decode(r)) match {
- case Some(r1) if !r1.is_singularity => Some(r1)
- case _ => None
- }
- in(symbol_range) orElse in(symbol_range - 1)
- }
- }
-
-
/* perspective */
object Perspective
--- a/src/Pure/Thy/html.scala Sat Apr 26 14:53:22 2014 +0200
+++ b/src/Pure/Thy/html.scala Sat Apr 26 22:57:51 2014 +0200
@@ -1,5 +1,5 @@
/* Title: Pure/Thy/html.scala
- Module: PIDE-GUI
+ Module: PIDE
Author: Makarius
HTML presentation elements.
@@ -8,9 +8,6 @@
package isabelle
-import scala.collection.mutable.ListBuffer
-
-
object HTML
{
/* encode text */
--- a/src/Pure/Tools/find_consts.ML Sat Apr 26 14:53:22 2014 +0200
+++ b/src/Pure/Tools/find_consts.ML Sat Apr 26 22:57:51 2014 +0200
@@ -11,6 +11,7 @@
Strict of string
| Loose of string
| Name of string
+ val read_query: Position.T -> string -> (bool * criterion) list
val find_consts : Proof.context -> (bool * criterion) list -> unit
end;
@@ -69,7 +70,7 @@
(* find_consts *)
-fun find_consts ctxt raw_criteria =
+fun pretty_consts ctxt raw_criteria =
let
val thy = Proof_Context.theory_of ctxt;
val low_ranking = 10000;
@@ -119,8 +120,10 @@
then "nothing found"
else "found " ^ string_of_int (length matches) ^ " constant(s):") ::
Pretty.str "" ::
- map (pretty_const ctxt) matches
- end |> Pretty.fbreaks |> curry Pretty.blk 0 |> Pretty.writeln;
+ map (Pretty.item o single o pretty_const ctxt) matches
+ end |> Pretty.fbreaks |> curry Pretty.blk 0;
+
+fun find_consts ctxt args = Pretty.writeln (pretty_consts ctxt args);
(* command syntax *)
@@ -132,15 +135,37 @@
Parse.reserved "name" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Name ||
Parse.xname >> Loose;
+val query = Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion);
+
in
+fun read_query pos str =
+ Outer_Syntax.scan pos str
+ |> filter Token.is_proper
+ |> Scan.error (Scan.finite Token.stopper (Parse.!!! (query --| Scan.ahead Parse.eof)))
+ |> #1;
+
val _ =
Outer_Syntax.improper_command @{command_spec "find_consts"}
- "find constants by name/type patterns"
- (Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion)
- >> (fn spec => Toplevel.keep (fn state => find_consts (Toplevel.context_of state) spec)));
+ "find constants by name / type patterns"
+ (query >> (fn spec =>
+ Toplevel.keep (fn st =>
+ Pretty.writeln (pretty_consts (Toplevel.context_of st) spec))));
end;
+
+(* PIDE query operation *)
+
+val _ =
+ Query_Operation.register "find_consts" (fn {state, args, output_result} =>
+ (case try Toplevel.context_of state of
+ SOME ctxt =>
+ let
+ val [query_arg] = args;
+ val query = read_query Position.none query_arg;
+ in output_result (Pretty.string_of (pretty_consts ctxt query)) end
+ | NONE => error "Unknown context"));
+
end;
--- a/src/Tools/jEdit/src/document_model.scala Sat Apr 26 14:53:22 2014 +0200
+++ b/src/Tools/jEdit/src/document_model.scala Sat Apr 26 22:57:51 2014 +0200
@@ -138,7 +138,7 @@
/* blob */
- private var _blob: Option[(Bytes, Text.Chunk)] = None // owned by Swing thread
+ private var _blob: Option[(Bytes, Symbol.Text_Chunk)] = None // owned by Swing thread
private def reset_blob(): Unit = Swing_Thread.require { _blob = None }
@@ -151,7 +151,7 @@
case Some(x) => x
case None =>
val bytes = PIDE.resources.file_content(buffer)
- val chunk = Text.Chunk(buffer.getSegment(0, buffer.getLength))
+ val chunk = Symbol.Text_Chunk(buffer.getSegment(0, buffer.getLength))
_blob = Some((bytes, chunk))
(bytes, chunk)
}
--- a/src/Tools/jEdit/src/find_dockable.scala Sat Apr 26 14:53:22 2014 +0200
+++ b/src/Tools/jEdit/src/find_dockable.scala Sat Apr 26 22:57:51 2014 +0200
@@ -9,26 +9,59 @@
import isabelle._
-import scala.swing.{Button, Component, TextField, CheckBox, Label, ComboBox}
-import scala.swing.event.ButtonClicked
+import java.awt.event.{ComponentEvent, ComponentAdapter, KeyEvent}
+import javax.swing.{JComponent, JTextField}
-import java.awt.BorderLayout
-import java.awt.event.{ComponentEvent, ComponentAdapter, KeyEvent}
+import scala.swing.{Button, Component, TextField, CheckBox, Label,
+ ComboBox, TabbedPane, BorderPanel}
+import scala.swing.event.{SelectionChanged, ButtonClicked, Key, KeyPressed}
import org.gjt.sp.jedit.View
+object Find_Dockable
+{
+ private abstract class Operation(view: View)
+ {
+ val pretty_text_area = new Pretty_Text_Area(view)
+ def query_operation: Query_Operation[View]
+ def query: JComponent
+ def select: Unit
+ def page: TabbedPane.Page
+ }
+}
+
class Find_Dockable(view: View, position: String) extends Dockable(view, position)
{
- val pretty_text_area = new Pretty_Text_Area(view)
- set_content(pretty_text_area)
+ /* common GUI components */
+
+ private var zoom_factor = 100
+
+ private val zoom =
+ new GUI.Zoom_Box(factor => if (zoom_factor != factor) { zoom_factor = factor; handle_resize() })
+ {
+ tooltip = "Zoom factor for output font size"
+ }
- /* query operation */
+ private def make_query(property: String, tooltip: String, apply_query: () => Unit): JTextField =
+ new Completion_Popup.History_Text_Field(property)
+ {
+ override def processKeyEvent(evt: KeyEvent)
+ {
+ if (evt.getID == KeyEvent.KEY_PRESSED && evt.getKeyCode == KeyEvent.VK_ENTER) apply_query()
+ super.processKeyEvent(evt)
+ }
+ { val max = getPreferredSize; max.width = Integer.MAX_VALUE; setMaximumSize(max) }
+ setColumns(40)
+ setToolTipText(tooltip)
+ setFont(GUI.imitate_font(Font_Info.main_family(), getFont, 1.2))
+ }
- private val process_indicator = new Process_Indicator
- private def consume_status(status: Query_Operation.Status.Value)
+ /* consume status */
+
+ def consume_status(process_indicator: Process_Indicator, status: Query_Operation.Status.Value)
{
status match {
case Query_Operation.Status.WAITING =>
@@ -40,23 +73,152 @@
}
}
- private val find_theorems =
- new Query_Operation(PIDE.editor, view, "find_theorems", consume_status _,
- (snapshot, results, body) =>
- pretty_text_area.update(snapshot, results, Pretty.separate(body)))
+
+ /* find theorems */
+
+ private val find_theorems = new Find_Dockable.Operation(view)
+ {
+ /* query */
+
+ private val process_indicator = new Process_Indicator
+
+ val query_operation =
+ new Query_Operation(PIDE.editor, view, "find_theorems",
+ consume_status(process_indicator, _),
+ (snapshot, results, body) =>
+ pretty_text_area.update(snapshot, results, Pretty.separate(body)))
+
+ private def apply_query()
+ {
+ query_operation.apply_query(List(limit.text, allow_dups.selected.toString, query.getText))
+ }
+
+ private val query_label = new Label("Search criteria:") {
+ tooltip =
+ GUI.tooltip_lines(
+ "Search criteria for find operation, e.g.\n\"_ = _\" \"op +\" name: Group -name: monoid")
+ }
+
+ val query = make_query("isabelle-find-theorems", query_label.tooltip, apply_query _)
+
+
+ /* GUI page */
+
+ private val limit = new TextField(PIDE.options.int("find_theorems_limit").toString, 5) {
+ tooltip = "Limit of displayed results"
+ verifier = (s: String) =>
+ s match { case Properties.Value.Int(x) => x >= 0 case _ => false }
+ listenTo(keys)
+ reactions += { case KeyPressed(_, Key.Enter, 0, _) => apply_query() }
+ }
+
+ private val allow_dups = new CheckBox("Duplicates") {
+ tooltip = "Show all versions of matching theorems"
+ selected = false
+ }
+
+ private val apply_button = new Button("Apply") {
+ tooltip = "Find theorems meeting specified criteria"
+ reactions += { case ButtonClicked(_) => apply_query() }
+ }
+
+ private val control_panel =
+ new Wrap_Panel(Wrap_Panel.Alignment.Right)(
+ query_label, Component.wrap(query), limit, allow_dups,
+ process_indicator.component, apply_button)
+
+ def select { control_panel.contents += zoom }
+
+ val page =
+ new TabbedPane.Page("Theorems", new BorderPanel {
+ add(control_panel, BorderPanel.Position.North)
+ add(Component.wrap(pretty_text_area), BorderPanel.Position.Center)
+ }, apply_button.tooltip)
+ }
+
+
+ /* find consts */
+
+ private val find_consts = new Find_Dockable.Operation(view)
+ {
+ /* query */
+
+ private val process_indicator = new Process_Indicator
+
+ val query_operation =
+ new Query_Operation(PIDE.editor, view, "find_consts",
+ consume_status(process_indicator, _),
+ (snapshot, results, body) =>
+ pretty_text_area.update(snapshot, results, Pretty.separate(body)))
+
+ private def apply_query()
+ {
+ query_operation.apply_query(List(query.getText))
+ }
+
+ private val query_label = new Label("Search criteria:") {
+ tooltip = GUI.tooltip_lines("Name / type patterns for constants")
+ }
+
+ val query = make_query("isabelle-find-consts", query_label.tooltip, apply_query _)
+
+
+ /* GUI page */
+
+ private val apply_button = new Button("Apply") {
+ tooltip = "Find constants by name / type patterns"
+ reactions += { case ButtonClicked(_) => apply_query() }
+ }
+
+ private val control_panel =
+ new Wrap_Panel(Wrap_Panel.Alignment.Right)(
+ query_label, Component.wrap(query), process_indicator.component, apply_button)
+
+ def select { control_panel.contents += zoom }
+
+ val page =
+ new TabbedPane.Page("Constants", new BorderPanel {
+ add(control_panel, BorderPanel.Position.North)
+ add(Component.wrap(pretty_text_area), BorderPanel.Position.Center)
+ }, apply_button.tooltip)
+ }
+
+
+ /* operations */
+
+ private val operations = List(find_theorems, find_consts)
+
+ private val operations_pane = new TabbedPane
+ {
+ pages ++= operations.map(_.page)
+ listenTo(selection)
+ reactions += { case SelectionChanged(_) => select_operation() }
+ }
+
+ private def get_operation(): Option[Find_Dockable.Operation] =
+ try { Some(operations(operations_pane.selection.index)) }
+ catch { case _: IndexOutOfBoundsException => None }
+
+ private def select_operation() {
+ for (op <- get_operation()) op.select
+ operations_pane.revalidate
+ }
+
+ override def focusOnDefaultComponent { for (op <- get_operation()) op.query.requestFocus }
+
+ select_operation()
+ set_content(operations_pane)
/* resize */
- private var zoom_factor = 100
-
- private def handle_resize()
- {
- Swing_Thread.require {}
-
- pretty_text_area.resize(
- Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom_factor / 100))
- }
+ private def handle_resize(): Unit =
+ Swing_Thread.require {
+ for (op <- operations) {
+ op.pretty_text_area.resize(
+ Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom_factor / 100))
+ }
+ }
private val delay_resize =
Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
@@ -77,67 +239,14 @@
{
PIDE.session.global_options += main
handle_resize()
- find_theorems.activate()
+ operations.foreach(op => op.query_operation.activate())
}
override def exit()
{
- find_theorems.deactivate()
+ operations.foreach(op => op.query_operation.deactivate())
PIDE.session.global_options -= main
delay_resize.revoke()
}
-
-
- /* controls */
-
- private def clicked
- {
- find_theorems.apply_query(List(limit.text, allow_dups.selected.toString, query.getText))
- }
-
- private val query_label = new Label("Search criteria:") {
- tooltip =
- GUI.tooltip_lines(
- "Search criteria for find operation, e.g.\n\"_ = _\" \"op +\" name: Group -name: monoid")
- }
-
- private val query = new Completion_Popup.History_Text_Field("isabelle-find-theorems") {
- override def processKeyEvent(evt: KeyEvent)
- {
- if (evt.getID == KeyEvent.KEY_PRESSED && evt.getKeyCode == KeyEvent.VK_ENTER) clicked
- super.processKeyEvent(evt)
- }
- { val max = getPreferredSize; max.width = Integer.MAX_VALUE; setMaximumSize(max) }
- setColumns(40)
- setToolTipText(query_label.tooltip)
- setFont(GUI.imitate_font(Font_Info.main_family(), getFont, 1.2))
- }
+}
- private val limit = new TextField(PIDE.options.int("find_theorems_limit").toString, 5) {
- tooltip = "Limit of displayed results"
- verifier = (s: String) =>
- s match { case Properties.Value.Int(x) => x >= 0 case _ => false }
- }
-
- private val allow_dups = new CheckBox("Duplicates") {
- tooltip = "Show all versions of matching theorems"
- selected = false
- }
-
- private val apply_query = new Button("Apply") {
- tooltip = "Find theorems meeting specified criteria"
- reactions += { case ButtonClicked(_) => clicked }
- }
-
- private val zoom = new GUI.Zoom_Box(factor => { zoom_factor = factor; handle_resize() }) {
- tooltip = "Zoom factor for output font size"
- }
-
- private val controls =
- new Wrap_Panel(Wrap_Panel.Alignment.Right)(
- query_label, Component.wrap(query), limit, allow_dups,
- process_indicator.component, apply_query, zoom)
- add(controls.peer, BorderLayout.NORTH)
-
- override def focusOnDefaultComponent { query.requestFocus }
-}
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala Sat Apr 26 14:53:22 2014 +0200
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Sat Apr 26 22:57:51 2014 +0200
@@ -162,7 +162,7 @@
val markup =
snapshot.state.command_markup(
snapshot.version, command, Command.Markup_Index.markup,
- command.range, Document.Elements.full)
+ command.range, Markup.Elements.full)
Isabelle_Sidekick.swing_markup_tree(markup, root, (info: Text.Info[List[XML.Elem]]) =>
{
val range = info.range + command_start
--- a/src/Tools/jEdit/src/jedit_options.scala Sat Apr 26 14:53:22 2014 +0200
+++ b/src/Tools/jEdit/src/jedit_options.scala Sat Apr 26 22:57:51 2014 +0200
@@ -93,6 +93,7 @@
case _ => true
}
})
+ GUI.plain_focus_traversal(text_area.peer)
text_area
}
component.load()
--- a/src/Tools/jEdit/src/rendering.scala Sat Apr 26 14:53:22 2014 +0200
+++ b/src/Tools/jEdit/src/rendering.scala Sat Apr 26 22:57:51 2014 +0200
@@ -129,28 +129,28 @@
/* markup elements */
private val semantic_completion_elements =
- Document.Elements(Markup.COMPLETION, Markup.NO_COMPLETION)
+ Markup.Elements(Markup.COMPLETION, Markup.NO_COMPLETION)
private val language_context_elements =
- Document.Elements(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM,
+ Markup.Elements(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM,
Markup.CARTOUCHE, Markup.COMMENT, Markup.LANGUAGE,
Markup.ML_STRING, Markup.ML_COMMENT)
private val highlight_elements =
- Document.Elements(Markup.LANGUAGE, Markup.ML_TYPING, Markup.TOKEN_RANGE,
+ Markup.Elements(Markup.LANGUAGE, Markup.ML_TYPING, Markup.TOKEN_RANGE,
Markup.ENTITY, Markup.PATH, Markup.URL, Markup.SORTING,
Markup.TYPING, Markup.FREE, Markup.SKOLEM, Markup.BOUND,
Markup.VAR, Markup.TFREE, Markup.TVAR)
private val hyperlink_elements =
- Document.Elements(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.URL)
+ Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.URL)
private val active_elements =
- Document.Elements(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW,
+ Markup.Elements(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW,
Markup.SENDBACK, Markup.SIMP_TRACE)
private val tooltip_message_elements =
- Document.Elements(Markup.WRITELN, Markup.WARNING, Markup.ERROR, Markup.BAD)
+ Markup.Elements(Markup.WRITELN, Markup.WARNING, Markup.ERROR, Markup.BAD)
private val tooltip_descriptions =
Map(
@@ -163,23 +163,23 @@
Markup.TVAR -> "schematic type variable")
private val tooltip_elements =
- Document.Elements(Markup.LANGUAGE, Markup.TIMING, Markup.ENTITY, Markup.SORTING,
+ Markup.Elements(Markup.LANGUAGE, Markup.TIMING, Markup.ENTITY, Markup.SORTING,
Markup.TYPING, Markup.ML_TYPING, Markup.PATH, Markup.URL) ++
- Document.Elements(tooltip_descriptions.keySet)
+ Markup.Elements(tooltip_descriptions.keySet)
private val gutter_elements =
- Document.Elements(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
+ Markup.Elements(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
private val squiggly_elements =
- Document.Elements(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
+ Markup.Elements(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
private val line_background_elements =
- Document.Elements(Markup.WRITELN_MESSAGE, Markup.TRACING_MESSAGE,
+ Markup.Elements(Markup.WRITELN_MESSAGE, Markup.TRACING_MESSAGE,
Markup.WARNING_MESSAGE, Markup.ERROR_MESSAGE,
Markup.INFORMATION)
private val separator_elements =
- Document.Elements(Markup.SEPARATOR)
+ Markup.Elements(Markup.SEPARATOR)
private val background_elements =
Protocol.proper_status_elements + Markup.WRITELN_MESSAGE +
@@ -188,14 +188,14 @@
active_elements
private val foreground_elements =
- Document.Elements(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM,
+ Markup.Elements(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM,
Markup.CARTOUCHE, Markup.ANTIQUOTED)
private val bullet_elements =
- Document.Elements(Markup.BULLET)
+ Markup.Elements(Markup.BULLET)
private val fold_depth_elements =
- Document.Elements(Markup.TEXT_FOLD, Markup.GOAL, Markup.SUBGOAL)
+ Markup.Elements(Markup.TEXT_FOLD, Markup.GOAL, Markup.SUBGOAL)
}
@@ -287,7 +287,7 @@
/* spell checker */
private lazy val spell_checker_elements =
- Document.Elements(space_explode(',', options.string("spell_checker_elements")): _*)
+ Markup.Elements(space_explode(',', options.string("spell_checker_elements")): _*)
def spell_checker_ranges(range: Text.Range): List[Text.Range] =
snapshot.select(range, spell_checker_elements, _ => _ => Some(())).map(_.range)
@@ -407,7 +407,7 @@
def command_results(range: Text.Range): Command.Results =
Command.State.merge_results(
- snapshot.select[List[Command.State]](range, Document.Elements.full, command_states =>
+ snapshot.select[List[Command.State]](range, Markup.Elements.full, command_states =>
{ case _ => Some(command_states) }).flatMap(_.info))
@@ -695,7 +695,7 @@
Markup.SML_COMMENT -> inner_comment_color)
private lazy val text_color_elements =
- Document.Elements(text_colors.keySet)
+ Markup.Elements(text_colors.keySet)
def text_color(range: Text.Range, color: Color): List[Text.Info[Color]] =
{
--- a/src/Tools/jEdit/src/simplifier_trace_window.scala Sat Apr 26 14:53:22 2014 +0200
+++ b/src/Tools/jEdit/src/simplifier_trace_window.scala Sat Apr 26 22:57:51 2014 +0200
@@ -207,9 +207,7 @@
val use_regex = new CheckBox("Regex")
private val controls = new Wrap_Panel(Wrap_Panel.Alignment.Right)(
- new Label {
- text = "Search"
- },
+ new Label("Search"),
new TextField(30) {
listenTo(keys)
reactions += {
--- a/src/Tools/jEdit/src/symbols_dockable.scala Sat Apr 26 14:53:22 2014 +0200
+++ b/src/Tools/jEdit/src/symbols_dockable.scala Sat Apr 26 22:57:51 2014 +0200
@@ -9,9 +9,7 @@
import isabelle._
-import java.awt.Font
-
-import scala.swing.event.ValueChanged
+import scala.swing.event.{SelectionChanged, ValueChanged}
import scala.swing.{Action, Button, TabbedPane, TextField, BorderPanel, Label, ScrollPane}
import org.gjt.sp.jedit.View
@@ -19,10 +17,6 @@
class Symbols_Dockable(view: View, position: String) extends Dockable(view, position)
{
- val searchspace =
- for ((group, symbols) <- Symbol.groups; sym <- symbols)
- yield (sym, Word.lowercase(sym))
-
private class Symbol_Component(val symbol: String) extends Button
{
private val decoded = Symbol.decode(symbol)
@@ -56,39 +50,52 @@
tooltip = "Reset control symbols within text"
}
- val group_tabs: TabbedPane = new TabbedPane {
+ private val group_tabs: TabbedPane = new TabbedPane {
pages ++=
- Symbol.groups map { case (group, symbols) =>
+ Symbol.groups.map({ case (group, symbols) =>
new TabbedPane.Page(group,
new ScrollPane(new Wrap_Panel {
contents ++= symbols.map(new Symbol_Component(_))
if (group == "control") contents += new Reset_Component
}), null)
- }
- pages += new TabbedPane.Page("search", new BorderPanel {
- val search = new TextField(10)
- val results_panel = new Wrap_Panel
- add(search, BorderPanel.Position.North)
- add(new ScrollPane(results_panel), BorderPanel.Position.Center)
- listenTo(search)
- val delay_search =
- Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) {
- val max_results = PIDE.options.int("jedit_symbols_search_limit") max 0
- results_panel.contents.clear
- val results =
- (searchspace filter
- (Word.explode(Word.lowercase(search.text)) forall _._2.contains)
- take (max_results + 1)).toList
- for ((sym, _) <- results)
- results_panel.contents += new Symbol_Component(sym)
- if (results.length > max_results) results_panel.contents += new Label("...")
- revalidate
- repaint
- }
- reactions += { case ValueChanged(`search`) => delay_search.invoke() }
- }, "Search Symbols")
- pages.map(p =>
- p.title = Word.implode(Word.explode('_', p.title).map(Word.perhaps_capitalize(_))))
+ })
+
+ val search_field = new TextField(10)
+ val search_page =
+ new TabbedPane.Page("search", new BorderPanel {
+ val results_panel = new Wrap_Panel
+ add(search_field, BorderPanel.Position.North)
+ add(new ScrollPane(results_panel), BorderPanel.Position.Center)
+
+ val search_space =
+ (for (sym <- Symbol.names.keysIterator) yield (sym, Word.lowercase(sym))).toList
+ val delay_search =
+ Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) {
+ val search_words = Word.explode(Word.lowercase(search_field.text))
+ val search_limit = PIDE.options.int("jedit_symbols_search_limit") max 0
+ val results =
+ for ((sym, s) <- search_space; if search_words.forall(s.contains(_))) yield sym
+
+ results_panel.contents.clear
+ for (sym <- results.take(search_limit))
+ results_panel.contents += new Symbol_Component(sym)
+ if (results.length > search_limit)
+ results_panel.contents +=
+ new Label("...") { tooltip = "(" + (results.length - search_limit) + " more)" }
+ revalidate
+ repaint
+ }
+ search_field.reactions += { case ValueChanged(_) => delay_search.invoke() }
+ }, "Search Symbols")
+ pages += search_page
+
+ listenTo(selection)
+ reactions += {
+ case SelectionChanged(_) if selection.page == search_page => search_field.requestFocus
+ }
+
+ for (page <- pages)
+ page.title = Word.implode(Word.explode('_', page.title).map(Word.perhaps_capitalize(_)))
}
set_content(group_tabs)
}