--- a/src/Pure/PIDE/document.scala Wed Aug 07 11:17:06 2013 +0200
+++ b/src/Pure/PIDE/document.scala Wed Aug 07 11:44:17 2013 +0200
@@ -15,48 +15,6 @@
{
/** document structure **/
- /* overlays -- print functions with arguments */
-
- type Overlay = (Command, (String, List[String]))
-
- object Overlays
- {
- val empty = new Overlays(Map.empty)
- }
-
- final class Overlays private(rep: Map[Command, List[(String, List[String])]])
- {
- def commands: Set[Command] = rep.keySet
- def is_empty: Boolean = rep.isEmpty
-
- def insert(cmd: Command, fn: (String, List[String])): Overlays =
- {
- val fns = rep.get(cmd) getOrElse Nil
- if (fns.contains(fn)) this
- else new Overlays(rep + (cmd -> (fn :: fns)))
- }
-
- def remove(cmd: Command, fn: (String, List[String])): Overlays =
- rep.get(cmd) match {
- case Some(fns) =>
- if (fns.contains(fn)) {
- fns.filterNot(_ == fn) match {
- case Nil => new Overlays(rep - cmd)
- case fns1 => new Overlays(rep + (cmd -> fns1))
- }
- }
- else this
- case None => this
- }
-
- def dest: List[Overlay] =
- (for {
- (cmd, fns) <- rep.iterator
- fn <- fns
- } yield (cmd, fn)).toList
- }
-
-
/* individual nodes */
type Edit[A, B] = (Node.Name, Node.Edit[A, B])
@@ -65,6 +23,11 @@
object Node
{
+ val empty: Node = new Node()
+
+
+ /* header and name */
+
sealed case class Header(
imports: List[Name],
keywords: Thy_Header.Keywords,
@@ -84,6 +47,7 @@
def compare(name1: Name, name2: Name): Int = name1.node compare name2.node
}
}
+
sealed case class Name(node: String, dir: String, theory: String)
{
override def hashCode: Int = node.hashCode
@@ -95,6 +59,51 @@
override def toString: String = theory
}
+
+ /* overlays -- print functions with arguments */
+
+ type Overlay = (Command, (String, List[String]))
+
+ object Overlays
+ {
+ val empty = new Overlays(Map.empty)
+ }
+
+ final class Overlays private(rep: Map[Command, List[(String, List[String])]])
+ {
+ def commands: Set[Command] = rep.keySet
+ def is_empty: Boolean = rep.isEmpty
+
+ def insert(cmd: Command, over: (String, List[String])): Overlays =
+ {
+ val overs = rep.getOrElse(cmd, Nil)
+ if (overs.contains(over)) this
+ else new Overlays(rep + (cmd -> (over :: overs)))
+ }
+
+ def remove(cmd: Command, over: (String, List[String])): Overlays =
+ rep.get(cmd) match {
+ case Some(overs) =>
+ if (overs.contains(over)) {
+ overs.filterNot(_ == over) match {
+ case Nil => new Overlays(rep - cmd)
+ case overs1 => new Overlays(rep + (cmd -> overs1))
+ }
+ }
+ else this
+ case None => this
+ }
+
+ def dest: List[Overlay] =
+ (for {
+ (cmd, overs) <- rep.iterator
+ over <- overs
+ } yield (cmd, over)).toList
+ }
+
+
+ /* edits */
+
sealed abstract class Edit[A, B]
{
def foreach(f: A => Unit)
@@ -112,6 +121,9 @@
type Perspective_Text = Perspective[Text.Edit, Text.Perspective]
type Perspective_Command = Perspective[Command.Edit, Command.Perspective]
+
+ /* commands */
+
def command_starts(commands: Iterator[Command], offset: Text.Offset = 0)
: Iterator[(Command, Text.Offset)] =
{
@@ -124,14 +136,12 @@
}
private val block_size = 1024
-
- val empty: Node = new Node()
}
final class Node private(
val header: Node.Header = Node.bad_header("Bad theory header"),
val perspective: Node.Perspective_Command =
- Node.Perspective(false, Command.Perspective.empty, Overlays.empty),
+ Node.Perspective(false, Command.Perspective.empty, Node.Overlays.empty),
val commands: Linear_Set[Command] = Linear_Set.empty)
{
def clear: Node = new Node(header = header)
--- a/src/Pure/Thy/thy_syntax.scala Wed Aug 07 11:17:06 2013 +0200
+++ b/src/Pure/Thy/thy_syntax.scala Wed Aug 07 11:44:17 2013 +0200
@@ -95,7 +95,7 @@
def command_perspective(
node: Document.Node,
perspective: Text.Perspective,
- overlays: Document.Overlays): (Command.Perspective, Command.Perspective) =
+ overlays: Document.Node.Overlays): (Command.Perspective, Command.Perspective) =
{
if (perspective.is_empty && overlays.is_empty)
(Command.Perspective.empty, Command.Perspective.empty)
--- a/src/Tools/jEdit/src/document_model.scala Wed Aug 07 11:17:06 2013 +0200
+++ b/src/Tools/jEdit/src/document_model.scala Wed Aug 07 11:44:17 2013 +0200
@@ -79,7 +79,7 @@
/* overlays */
- private var overlays = Document.Overlays.empty
+ private var overlays = Document.Node.Overlays.empty
def insert_overlay(command: Command, name: String, args: List[String]): Unit =
Swing_Thread.require { overlays = overlays.insert(command, (name, args)) }
@@ -104,7 +104,7 @@
}
val empty_perspective: Document.Node.Perspective_Text =
- Document.Node.Perspective(false, Text.Perspective.empty, Document.Overlays.empty)
+ Document.Node.Perspective(false, Text.Perspective.empty, Document.Node.Overlays.empty)
def node_perspective(): Document.Node.Perspective_Text =
{