tuned signature;
authorwenzelm
Wed Aug 07 11:44:17 2013 +0200 (2013-08-07)
changeset 5288798eac7b7eec3
parent 52886 1e22e8101f47
child 52888 671421cef590
tuned signature;
src/Pure/PIDE/document.scala
src/Pure/Thy/thy_syntax.scala
src/Tools/jEdit/src/document_model.scala
     1.1 --- a/src/Pure/PIDE/document.scala	Wed Aug 07 11:17:06 2013 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Wed Aug 07 11:44:17 2013 +0200
     1.3 @@ -15,48 +15,6 @@
     1.4  {
     1.5    /** document structure **/
     1.6  
     1.7 -  /* overlays -- print functions with arguments */
     1.8 -
     1.9 -  type Overlay = (Command, (String, List[String]))
    1.10 -
    1.11 -  object Overlays
    1.12 -  {
    1.13 -    val empty = new Overlays(Map.empty)
    1.14 -  }
    1.15 -
    1.16 -  final class Overlays private(rep: Map[Command, List[(String, List[String])]])
    1.17 -  {
    1.18 -    def commands: Set[Command] = rep.keySet
    1.19 -    def is_empty: Boolean = rep.isEmpty
    1.20 -
    1.21 -    def insert(cmd: Command, fn: (String, List[String])): Overlays =
    1.22 -    {
    1.23 -      val fns = rep.get(cmd) getOrElse Nil
    1.24 -      if (fns.contains(fn)) this
    1.25 -      else new Overlays(rep + (cmd -> (fn :: fns)))
    1.26 -    }
    1.27 -
    1.28 -    def remove(cmd: Command, fn: (String, List[String])): Overlays =
    1.29 -      rep.get(cmd) match {
    1.30 -        case Some(fns) =>
    1.31 -          if (fns.contains(fn)) {
    1.32 -            fns.filterNot(_ == fn) match {
    1.33 -              case Nil => new Overlays(rep - cmd)
    1.34 -              case fns1 => new Overlays(rep + (cmd -> fns1))
    1.35 -            }
    1.36 -          }
    1.37 -          else this
    1.38 -        case None => this
    1.39 -      }
    1.40 -
    1.41 -    def dest: List[Overlay] =
    1.42 -      (for {
    1.43 -        (cmd, fns) <- rep.iterator
    1.44 -        fn <- fns
    1.45 -      } yield (cmd, fn)).toList
    1.46 -  }
    1.47 -
    1.48 -
    1.49    /* individual nodes */
    1.50  
    1.51    type Edit[A, B] = (Node.Name, Node.Edit[A, B])
    1.52 @@ -65,6 +23,11 @@
    1.53  
    1.54    object Node
    1.55    {
    1.56 +    val empty: Node = new Node()
    1.57 +
    1.58 +
    1.59 +    /* header and name */
    1.60 +
    1.61      sealed case class Header(
    1.62        imports: List[Name],
    1.63        keywords: Thy_Header.Keywords,
    1.64 @@ -84,6 +47,7 @@
    1.65          def compare(name1: Name, name2: Name): Int = name1.node compare name2.node
    1.66        }
    1.67      }
    1.68 +
    1.69      sealed case class Name(node: String, dir: String, theory: String)
    1.70      {
    1.71        override def hashCode: Int = node.hashCode
    1.72 @@ -95,6 +59,51 @@
    1.73        override def toString: String = theory
    1.74      }
    1.75  
    1.76 +
    1.77 +    /* overlays -- print functions with arguments */
    1.78 +
    1.79 +    type Overlay = (Command, (String, List[String]))
    1.80 +
    1.81 +    object Overlays
    1.82 +    {
    1.83 +      val empty = new Overlays(Map.empty)
    1.84 +    }
    1.85 +
    1.86 +    final class Overlays private(rep: Map[Command, List[(String, List[String])]])
    1.87 +    {
    1.88 +      def commands: Set[Command] = rep.keySet
    1.89 +      def is_empty: Boolean = rep.isEmpty
    1.90 +
    1.91 +      def insert(cmd: Command, over: (String, List[String])): Overlays =
    1.92 +      {
    1.93 +        val overs = rep.getOrElse(cmd, Nil)
    1.94 +        if (overs.contains(over)) this
    1.95 +        else new Overlays(rep + (cmd -> (over :: overs)))
    1.96 +      }
    1.97 +
    1.98 +      def remove(cmd: Command, over: (String, List[String])): Overlays =
    1.99 +        rep.get(cmd) match {
   1.100 +          case Some(overs) =>
   1.101 +            if (overs.contains(over)) {
   1.102 +              overs.filterNot(_ == over) match {
   1.103 +                case Nil => new Overlays(rep - cmd)
   1.104 +                case overs1 => new Overlays(rep + (cmd -> overs1))
   1.105 +              }
   1.106 +            }
   1.107 +            else this
   1.108 +          case None => this
   1.109 +        }
   1.110 +
   1.111 +      def dest: List[Overlay] =
   1.112 +        (for {
   1.113 +          (cmd, overs) <- rep.iterator
   1.114 +          over <- overs
   1.115 +        } yield (cmd, over)).toList
   1.116 +    }
   1.117 +
   1.118 +
   1.119 +    /* edits */
   1.120 +
   1.121      sealed abstract class Edit[A, B]
   1.122      {
   1.123        def foreach(f: A => Unit)
   1.124 @@ -112,6 +121,9 @@
   1.125      type Perspective_Text = Perspective[Text.Edit, Text.Perspective]
   1.126      type Perspective_Command = Perspective[Command.Edit, Command.Perspective]
   1.127  
   1.128 +
   1.129 +    /* commands */
   1.130 +
   1.131      def command_starts(commands: Iterator[Command], offset: Text.Offset = 0)
   1.132        : Iterator[(Command, Text.Offset)] =
   1.133      {
   1.134 @@ -124,14 +136,12 @@
   1.135      }
   1.136  
   1.137      private val block_size = 1024
   1.138 -
   1.139 -    val empty: Node = new Node()
   1.140    }
   1.141  
   1.142    final class Node private(
   1.143      val header: Node.Header = Node.bad_header("Bad theory header"),
   1.144      val perspective: Node.Perspective_Command =
   1.145 -      Node.Perspective(false, Command.Perspective.empty, Overlays.empty),
   1.146 +      Node.Perspective(false, Command.Perspective.empty, Node.Overlays.empty),
   1.147      val commands: Linear_Set[Command] = Linear_Set.empty)
   1.148    {
   1.149      def clear: Node = new Node(header = header)
     2.1 --- a/src/Pure/Thy/thy_syntax.scala	Wed Aug 07 11:17:06 2013 +0200
     2.2 +++ b/src/Pure/Thy/thy_syntax.scala	Wed Aug 07 11:44:17 2013 +0200
     2.3 @@ -95,7 +95,7 @@
     2.4    def command_perspective(
     2.5        node: Document.Node,
     2.6        perspective: Text.Perspective,
     2.7 -      overlays: Document.Overlays): (Command.Perspective, Command.Perspective) =
     2.8 +      overlays: Document.Node.Overlays): (Command.Perspective, Command.Perspective) =
     2.9    {
    2.10      if (perspective.is_empty && overlays.is_empty)
    2.11        (Command.Perspective.empty, Command.Perspective.empty)
     3.1 --- a/src/Tools/jEdit/src/document_model.scala	Wed Aug 07 11:17:06 2013 +0200
     3.2 +++ b/src/Tools/jEdit/src/document_model.scala	Wed Aug 07 11:44:17 2013 +0200
     3.3 @@ -79,7 +79,7 @@
     3.4  
     3.5    /* overlays */
     3.6  
     3.7 -  private var overlays = Document.Overlays.empty
     3.8 +  private var overlays = Document.Node.Overlays.empty
     3.9  
    3.10    def insert_overlay(command: Command, name: String, args: List[String]): Unit =
    3.11      Swing_Thread.require { overlays = overlays.insert(command, (name, args)) }
    3.12 @@ -104,7 +104,7 @@
    3.13    }
    3.14  
    3.15    val empty_perspective: Document.Node.Perspective_Text =
    3.16 -    Document.Node.Perspective(false, Text.Perspective.empty, Document.Overlays.empty)
    3.17 +    Document.Node.Perspective(false, Text.Perspective.empty, Document.Node.Overlays.empty)
    3.18  
    3.19    def node_perspective(): Document.Node.Perspective_Text =
    3.20    {