src/Pure/PIDE/document.scala
changeset 46677 388ba4daae05
parent 46208 4cab63a6dc16
child 46678 c2dba08548f9
     1.1 --- a/src/Pure/PIDE/document.scala	Sun Feb 26 15:18:48 2012 +0100
     1.2 +++ b/src/Pure/PIDE/document.scala	Sun Feb 26 16:02:53 2012 +0100
     1.3 @@ -82,8 +82,7 @@
     1.4          case exn => exn
     1.5        }
     1.6  
     1.7 -    val empty: Node =
     1.8 -      Node(Exn.Exn(ERROR("Bad theory header")), Command.Perspective.empty, Map(), Linear_Set())
     1.9 +    val empty: Node = Node()
    1.10  
    1.11      def command_starts(commands: Iterator[Command], offset: Text.Offset = 0)
    1.12        : Iterator[(Command, Text.Offset)] =
    1.13 @@ -100,10 +99,10 @@
    1.14    private val block_size = 1024
    1.15  
    1.16    sealed case class Node(
    1.17 -    val header: Node_Header,
    1.18 -    val perspective: Command.Perspective,
    1.19 -    val blobs: Map[String, Blob],
    1.20 -    val commands: Linear_Set[Command])
    1.21 +    val header: Node_Header = Exn.Exn(ERROR("Bad theory header")),
    1.22 +    val perspective: Command.Perspective = Command.Perspective.empty,
    1.23 +    val blobs: Map[String, Blob] = Map.empty,
    1.24 +    val commands: Linear_Set[Command] = Linear_Set.empty)
    1.25    {
    1.26      def clear: Node = Node.empty.copy(header = header)
    1.27  
    1.28 @@ -154,10 +153,7 @@
    1.29        }
    1.30  
    1.31      def command_start(cmd: Command): Option[Text.Offset] =
    1.32 -      command_starts.find(_._1 == cmd).map(_._2)
    1.33 -
    1.34 -    def command_starts: Iterator[(Command, Text.Offset)] =
    1.35 -      Node.command_starts(commands.iterator)
    1.36 +      Node.command_starts(commands.iterator).find(_._1 == cmd).map(_._2)
    1.37    }
    1.38  
    1.39  
    1.40 @@ -166,13 +162,16 @@
    1.41  
    1.42    /* particular document versions */
    1.43  
    1.44 +  type Nodes = Map[Node.Name, Node]
    1.45 +
    1.46    object Version
    1.47    {
    1.48 -    val init: Version = Version(no_id, Map().withDefaultValue(Node.empty))
    1.49 +    val init: Version = Version()
    1.50    }
    1.51  
    1.52 -  type Nodes = Map[Node.Name, Node]
    1.53 -  sealed case class Version(val id: Version_ID, val nodes: Nodes)
    1.54 +  sealed case class Version(
    1.55 +    val id: Version_ID = no_id,
    1.56 +    val nodes: Nodes = Map.empty.withDefaultValue(Node.empty))
    1.57    {
    1.58      def topological_order: List[Node.Name] =
    1.59      {
    1.60 @@ -192,13 +191,13 @@
    1.61  
    1.62    object Change
    1.63    {
    1.64 -    val init: Change = Change(Some(Future.value(Version.init)), Nil, Future.value(Version.init))
    1.65 +    val init: Change = Change()
    1.66    }
    1.67  
    1.68    sealed case class Change(
    1.69 -    val previous: Option[Future[Version]],
    1.70 -    val edits: List[Edit_Text],
    1.71 -    val version: Future[Version])
    1.72 +    val previous: Option[Future[Version]] = Some(Future.value(Version.init)),
    1.73 +    val edits: List[Edit_Text] = Nil,
    1.74 +    val version: Future[Version] = Future.value(Version.init))
    1.75    {
    1.76      def is_finished: Boolean =
    1.77        (previous match { case None => true case Some(future) => future.is_finished }) &&
    1.78 @@ -212,11 +211,11 @@
    1.79  
    1.80    object History
    1.81    {
    1.82 -    val init: History = History(List(Change.init))
    1.83 +    val init: History = History()
    1.84    }
    1.85  
    1.86    // FIXME pruning, purging of state
    1.87 -  sealed case class History(val undo_list: List[Change])
    1.88 +  sealed case class History(val undo_list: List[Change] = List(Change.init))
    1.89    {
    1.90      require(!undo_list.isEmpty)
    1.91  
    1.92 @@ -259,13 +258,13 @@
    1.93  
    1.94      object Assignment
    1.95      {
    1.96 -      val init: Assignment = Assignment(Map.empty, Map.empty, false)
    1.97 +      val init: Assignment = Assignment()
    1.98      }
    1.99  
   1.100      case class Assignment(
   1.101 -      val command_execs: Map[Command_ID, Exec_ID],
   1.102 -      val last_execs: Map[String, Option[Command_ID]],
   1.103 -      val is_finished: Boolean)
   1.104 +      val command_execs: Map[Command_ID, Exec_ID] = Map.empty,
   1.105 +      val last_execs: Map[String, Option[Command_ID]] = Map.empty,
   1.106 +      val is_finished: Boolean = false)
   1.107      {
   1.108        def check_finished: Assignment = { require(is_finished); this }
   1.109        def unfinished: Assignment = copy(is_finished = false)
   1.110 @@ -285,10 +284,10 @@
   1.111    }
   1.112  
   1.113    sealed case class State(
   1.114 -    val versions: Map[Version_ID, Version] = Map(),
   1.115 -    val commands: Map[Command_ID, Command.State] = Map(),  // static markup from define_command
   1.116 -    val execs: Map[Exec_ID, Command.State] = Map(),  // dynamic markup from execution
   1.117 -    val assignments: Map[Version_ID, State.Assignment] = Map(),
   1.118 +    val versions: Map[Version_ID, Version] = Map.empty,
   1.119 +    val commands: Map[Command_ID, Command.State] = Map.empty,  // static markup from define_command
   1.120 +    val execs: Map[Exec_ID, Command.State] = Map.empty,  // dynamic markup from execution
   1.121 +    val assignments: Map[Version_ID, State.Assignment] = Map.empty,
   1.122      val history: History = History.init)
   1.123    {
   1.124      private def fail[A]: A = throw new State.Fail(this)