src/Pure/PIDE/document.ML
changeset 52600 75afb82daf5c
parent 52599 d7871f38ffb4
child 52602 00170ef1dc39
     1.1 --- a/src/Pure/PIDE/document.ML	Thu Jul 11 16:01:48 2013 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Thu Jul 11 16:26:14 2013 +0200
     1.3 @@ -334,7 +334,7 @@
     1.4                  (fn () =>
     1.5                    iterate_entries (fn (_, opt_exec) => fn () =>
     1.6                      (case opt_exec of
     1.7 -                      SOME exec => if running () then SOME (Command.execute exec) else NONE
     1.8 +                      SOME exec => if running () then SOME (Command.exec exec) else NONE
     1.9                      | NONE => NONE)) node ()));
    1.10    in () end;
    1.11