author | wenzelm |
Fri, 04 Nov 2022 17:17:05 +0100 | |
changeset 76437 | 83cf8073a7bf |
parent 76436 | 9e5098cbf81f |
child 76438 | 34a10f5dde92 |
--- a/src/Pure/PIDE/document.ML Fri Nov 04 17:14:41 2022 +0100 +++ b/src/Pure/PIDE/document.ML Fri Nov 04 17:17:05 2022 +0100 @@ -725,7 +725,7 @@ if active then NONE else (case opt_exec of - NONE => NONE + NONE => SOME true | SOME (eval, _) => SOME (not (null (Execution.snapshot [Command.eval_exec_id eval]))))); fun presentation_context options the_command_span node_name node : Thy_Info.presentation_context =