tuned;
authorwenzelm
Fri, 04 Nov 2022 15:05:23 +0100
changeset 76428 82bd2cfafe4c
parent 76427 98bf45a5b508
child 76429 bd919b794b38
tuned;
src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Fri Nov 04 14:53:25 2022 +0100
+++ b/src/Pure/PIDE/document.ML	Fri Nov 04 15:05:23 2022 +0100
@@ -824,7 +824,7 @@
     val nodes = nodes_of new_version;
     val required = make_required nodes;
     val required0 = make_required (nodes_of old_version);
-    val edited = Symtab.build (edits |> fold (fn (name, _) => Symtab.update (name, ())));
+    val edited = Symtab.build (edits |> fold (Symtab.insert_set o #1));
 
     val updated = timeit "Document.update" (fn () =>
       nodes |> String_Graph.schedule