src/Pure/PIDE/document.ML
changeset 57616 50ab1db5c0fd
parent 57615 df1b3452d71c
child 57638 ed58e740a699
     1.1 --- a/src/Pure/PIDE/document.ML	Wed Jul 23 13:01:30 2014 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Wed Jul 23 14:50:20 2014 +0200
     1.3 @@ -223,7 +223,13 @@
     1.4      | Perspective perspective => update_node name (set_perspective perspective) nodes);
     1.5  
     1.6  fun put_node (name, node) (Version nodes) =
     1.7 -  Version (update_node name (K node) nodes);
     1.8 +  let
     1.9 +    val nodes1 = update_node name (K node) nodes;
    1.10 +    val nodes2 =
    1.11 +      if String_Graph.is_maximal nodes1 name andalso is_empty_node node
    1.12 +      then String_Graph.del_node name nodes1
    1.13 +      else nodes1;
    1.14 +  in Version nodes2 end;
    1.15  
    1.16  end;
    1.17