src/Pure/PIDE/document.ML
changeset 57615 df1b3452d71c
parent 56801 8dd9df88f647
child 57616 50ab1db5c0fd
     1.1 --- a/src/Pure/PIDE/document.ML	Wed Jul 23 11:53:34 2014 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Wed Jul 23 13:01:30 2014 +0200
     1.3 @@ -72,11 +72,23 @@
     1.4    visible_last = try List.last command_ids,
     1.5    overlays = Inttab.make_list overlays};
     1.6  
     1.7 -val no_header = ("", Thy_Header.make ("", Position.none) [] [], ["No theory header"]);
     1.8 +val no_header = ("", Thy_Header.make ("", Position.none) [] [], []);
     1.9  val no_perspective = make_perspective (false, [], []);
    1.10  
    1.11  val empty_node = make_node (no_header, no_perspective, Entries.empty, NONE);
    1.12  
    1.13 +fun is_no_perspective ({required, visible, visible_last, overlays}: perspective) =
    1.14 +  not required andalso
    1.15 +  Inttab.is_empty visible andalso
    1.16 +  is_none visible_last andalso
    1.17 +  Inttab.is_empty overlays;
    1.18 +
    1.19 +fun is_empty_node (Node {header, perspective, entries, result}) =
    1.20 +  header = no_header andalso
    1.21 +  is_no_perspective perspective andalso
    1.22 +  Entries.is_empty entries andalso
    1.23 +  is_none result;
    1.24 +
    1.25  
    1.26  (* basic components *)
    1.27