1.1 --- a/src/Pure/PIDE/command.ML	Tue Jul 09 16:32:51 2013 +0200
     1.2 +++ b/src/Pure/PIDE/command.ML	Tue Jul 09 17:58:38 2013 +0200
     1.3 @@ -13,7 +13,7 @@
     1.4    type print = {name: string, pri: int, exec_id: Document_ID.exec, print_process: print_process}
     1.5    type exec = eval * print list
     1.6    val no_exec: exec
     1.7 -  val exec_ids: exec -> Document_ID.exec list
     1.8 +  val exec_ids: exec option -> Document_ID.exec list
     1.9    val read: (unit -> theory) -> Token.T list -> Toplevel.transition
    1.10    val eval: (unit -> theory) -> Token.T list -> eval -> eval
    1.11    val print: string -> eval -> print list
    1.12 @@ -90,7 +90,8 @@
    1.13  type exec = eval * print list;
    1.14  val no_exec: exec = ({exec_id = Document_ID.none, eval_process = memo_value init_eval_state}, []);
    1.15  
    1.16 -fun exec_ids (({exec_id, ...}, prints): exec) = exec_id :: map #exec_id prints;
    1.17 +fun exec_ids (NONE: exec option) = []
    1.18 +  | exec_ids (SOME ({exec_id, ...}, prints)) = exec_id :: map #exec_id prints;
    1.19  
    1.20  
    1.21  (* read *)