src/Pure/PIDE/command.ML
changeset 53723 7a0935571a23
parent 53709 2fb1f9cf80d3
child 53733 40298d383463
     1.1 --- a/src/Pure/PIDE/command.ML	Wed Jul 10 23:30:10 2013 +0200
     1.2 +++ b/src/Pure/PIDE/command.ML	Thu Jul 11 10:43:53 2013 +0200
     1.3 @@ -18,6 +18,7 @@
     1.4    val exec_ids: exec option -> Document_ID.exec list
     1.5    val stable_eval: eval -> bool
     1.6    val stable_print: print -> bool
     1.7 +  val same_eval: eval * eval -> bool
     1.8    val read: (unit -> theory) -> Token.T list -> Toplevel.transition
     1.9    val eval: (unit -> theory) -> Token.T list -> eval -> eval
    1.10    val print: bool -> string -> eval -> print list -> print list option
    1.11 @@ -111,6 +112,9 @@
    1.12  fun stable_print ({exec_id, print_process, ...}: print) =
    1.13    stable_goals exec_id andalso memo_stable print_process;
    1.14  
    1.15 +fun same_eval (eval: eval, eval': eval) =
    1.16 +  #exec_id eval = #exec_id eval' andalso stable_eval eval';
    1.17 +
    1.18  
    1.19  (* read *)
    1.20