# HG changeset patch
# User wenzelm
# Date 1701268041 -3600
# Node ID 238c4acdf984e4c82782e856bc4ea006ba387814
# Parent  6b071d4041d59b5e405da605254e1d668f87b877
more compact representation;

diff -r 6b071d4041d5 -r 238c4acdf984 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Wed Nov 29 13:05:57 2023 +0100
+++ b/src/Pure/PIDE/document.ML	Wed Nov 29 15:27:21 2023 +0100
@@ -54,7 +54,7 @@
 
 type perspective =
  {required: bool,  (*required node*)
-  visible: Intset.T,  (*visible commands*)
+  visible: Bitset.T,  (*visible commands*)
   visible_last: Document_ID.command option,  (*last visible command*)
   overlays: (string * string list) list Inttab.table};  (*command id -> print functions with args*)
 
@@ -79,7 +79,7 @@
 
 fun make_perspective (required, command_ids, overlays) : perspective =
  {required = required,
-  visible = Intset.make command_ids,
+  visible = Bitset.make command_ids,
   visible_last = try List.last command_ids,
   overlays = Inttab.make_list overlays};
 
@@ -93,7 +93,7 @@
 
 fun is_empty_perspective ({required, visible, visible_last, overlays}: perspective) =
   not required andalso
-  Intset.is_empty visible andalso
+  Bitset.is_empty visible andalso
   is_none visible_last andalso
   Inttab.is_empty overlays;
 
@@ -147,7 +147,7 @@
 
 val required_node = #required o get_perspective;
 val command_overlays = Inttab.lookup_list o #overlays o get_perspective;
-val command_visible = Intset.member o #visible o get_perspective;
+val command_visible = Bitset.member o #visible o get_perspective;
 val visible_last = #visible_last o get_perspective;
 val visible_node = is_some o visible_last