src/Tools/jEdit/src/session_dockable.scala
changeset 45672 a497c5d4a523
parent 45665 129db1416717
child 45709 87017fcbad83
     1.1 --- a/src/Tools/jEdit/src/session_dockable.scala	Tue Nov 29 20:17:11 2011 +0100
     1.2 +++ b/src/Tools/jEdit/src/session_dockable.scala	Tue Nov 29 20:18:02 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, Isar_Document.Node_Status] = Map.empty
     1.8 +  private var nodes_status: Map[Document.Node.Name, Isabelle_Document.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 = Isar_Document.node_status(snapshot.state, snapshot.version, node)
    1.17 +        val status = Isabelle_Document.node_status(snapshot.state, snapshot.version, node)
    1.18        } nodes_status1 += (name -> status)
    1.19  
    1.20        if (nodes_status != nodes_status1) {