changeset 53743 | 0d68d108d7e0 |
parent 53742 | a2a805549c74 |
child 53744 | 33a133d50616 |
1.1 --- a/src/Pure/PIDE/command.ML Fri Jul 12 11:07:02 2013 +0200 1.2 +++ b/src/Pure/PIDE/command.ML Fri Jul 12 11:28:03 2013 +0200 1.3 @@ -20,7 +20,7 @@ 1.4 type exec = eval * print list 1.5 val no_exec: exec 1.6 val exec_ids: exec option -> Document_ID.exec list 1.7 - val exec: Execution.context -> exec -> unit 1.8 + val exec: Document_ID.execution -> exec -> unit 1.9 end; 1.10 1.11 structure Command: COMMAND =