Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
command 'redo' no longer available;
authorwenzelm
Mon, 14 Jul 2008 11:19:42 +0200
changeset 27565 4bb03d4509e2
parent 27564 fc6d34e49e17
child 27566 6b20092af078
command 'redo' no longer available;
src/Pure/ProofGeneral/proof_general_pgip.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Mon Jul 14 11:19:41 2008 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Mon Jul 14 11:19:42 2008 +0200
@@ -429,7 +429,7 @@
 fun isarcmd s = Isar.>>> (OuterSyntax.parse Position.none s);
 
 (* TODO:
-    - apply a command given a transition function, e.g. IsarCmd.undo.
+    - apply a command given a transition function;
     - fix position from path of currently open file [line numbers risk garbling though].
 *)
 
@@ -549,7 +549,7 @@
         isarcmd ("undos_proof " ^ Int.toString times)
     end
 
-fun redostep _ = isarcmd "redo"
+fun redostep _ = sys_error "redo unavailable"
 
 fun abortgoal _ = isarcmd "kill" (* was: ProofGeneral.kill_proof *)
isabelle