# HG changeset patch # User wenzelm # Date 1398545871 -7200 # Node ID 539fe017905a92ccf979a374be10f0d8f8422f8f # Parent 678a52e676b67c85316c6b57ed01ab2b344597f5# Parent 951c6a9ac3d7003168dad42c7dc70da8ca6757b0 merged diff -r 678a52e676b6 -r 539fe017905a NEWS --- 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 diff -r 678a52e676b6 -r 539fe017905a src/HOL/Hahn_Banach/Hahn_Banach.thy --- 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 \ 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 \ x) = \a\ * p x" proof - diff -r 678a52e676b6 -r 539fe017905a src/HOL/Hahn_Banach/Normed_Space.thy --- 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 "\\\"} 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 = diff -r 678a52e676b6 -r 539fe017905a src/Pure/GUI/gui.scala --- 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] = diff -r 678a52e676b6 -r 539fe017905a src/Pure/General/multi_map.scala --- 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. */ diff -r 678a52e676b6 -r 539fe017905a src/Pure/General/position.scala --- 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 diff -r 678a52e676b6 -r 539fe017905a src/Pure/General/symbol.scala --- 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)]) diff -r 678a52e676b6 -r 539fe017905a src/Pure/General/word.scala --- 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) } diff -r 678a52e676b6 -r 539fe017905a src/Pure/PIDE/command.scala --- 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 diff -r 678a52e676b6 -r 539fe017905a src/Pure/PIDE/document.scala --- 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]] = { diff -r 678a52e676b6 -r 539fe017905a src/Pure/PIDE/document_id.scala --- 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. diff -r 678a52e676b6 -r 539fe017905a src/Pure/PIDE/markup.ML --- 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 = diff -r 678a52e676b6 -r 539fe017905a src/Pure/PIDE/markup.scala --- 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" diff -r 678a52e676b6 -r 539fe017905a src/Pure/PIDE/markup_tree.scala --- 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 diff -r 678a52e676b6 -r 539fe017905a src/Pure/PIDE/protocol.scala --- 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] = diff -r 678a52e676b6 -r 539fe017905a src/Pure/PIDE/text.scala --- 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 diff -r 678a52e676b6 -r 539fe017905a src/Pure/Thy/html.scala --- 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 */ diff -r 678a52e676b6 -r 539fe017905a src/Pure/Tools/find_consts.ML --- 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; diff -r 678a52e676b6 -r 539fe017905a src/Tools/jEdit/src/document_model.scala --- 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) } diff -r 678a52e676b6 -r 539fe017905a src/Tools/jEdit/src/find_dockable.scala --- 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 } -} diff -r 678a52e676b6 -r 539fe017905a src/Tools/jEdit/src/isabelle_sidekick.scala --- 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 diff -r 678a52e676b6 -r 539fe017905a src/Tools/jEdit/src/jedit_options.scala --- 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() diff -r 678a52e676b6 -r 539fe017905a src/Tools/jEdit/src/rendering.scala --- 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]] = { diff -r 678a52e676b6 -r 539fe017905a src/Tools/jEdit/src/simplifier_trace_window.scala --- 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 += { diff -r 678a52e676b6 -r 539fe017905a src/Tools/jEdit/src/symbols_dockable.scala --- 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) }