changeset 74166 | ff3dbb2be924 |
parent 73761 | ef1a18e20ace |
child 74673 | eae5fa0055bd |
--- a/src/Pure/PIDE/command.ML Sun Aug 22 17:52:27 2021 +0200 +++ b/src/Pure/PIDE/command.ML Sun Aug 22 19:21:54 2021 +0200 @@ -95,7 +95,7 @@ let val file_pos = Position.file file_node |> - (case Position.get_id (Position.thread_data ()) of + (case Position.id_of (Position.thread_data ()) of NONE => I | SOME exec_id => Position.put_id exec_id); in {src_path = src_path, lines = lines, digest = digest, pos = file_pos} end