src/Tools/jEdit/src/session_dockable.scala
changeset 45709 87017fcbad83
parent 45672 a497c5d4a523
child 46681 c083a3f621c0
     1.1 --- a/src/Tools/jEdit/src/session_dockable.scala	Thu Dec 01 13:34:16 2011 +0100
     1.2 +++ b/src/Tools/jEdit/src/session_dockable.scala	Thu Dec 01 14:29:14 2011 +0100
     1.3 @@ -94,7 +94,7 @@
     1.4  
     1.5    /* component state -- owned by Swing thread */
     1.6  
     1.7 -  private var nodes_status: Map[Document.Node.Name, Isabelle_Document.Node_Status] = Map.empty
     1.8 +  private var nodes_status: Map[Document.Node.Name, Protocol.Node_Status] = Map.empty
     1.9  
    1.10    private object Node_Renderer_Component extends Label
    1.11    {
    1.12 @@ -152,7 +152,7 @@
    1.13        for {
    1.14          name <- nodes
    1.15          node <- snapshot.version.nodes.get(name)
    1.16 -        val status = Isabelle_Document.node_status(snapshot.state, snapshot.version, node)
    1.17 +        val status = Protocol.node_status(snapshot.state, snapshot.version, node)
    1.18        } nodes_status1 += (name -> status)
    1.19  
    1.20        if (nodes_status != nodes_status1) {