From 6a52ce4da196e146db2d2e551362c4c5c38a9ab3 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Fri, 9 Oct 1998 13:41:34 +0000 Subject: Added todos for: rsh, multi file failure, multi file in Isabelle, splash. --- todo | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/todo b/todo index 7b7e7169..d9c37bfb 100644 --- a/todo +++ b/todo @@ -22,6 +22,11 @@ B proof-find-next-terminator doesn't work properly: move point to "t". Currently, it doesn't do anything. This is a bug. +B Add proof-rsh-command and note in documentation about how to + use widely-advertised "remote shell" feature. (1hr) + +D Multiple files (after basic feature added): handle failures in + reading ancestors. A* Fix Non Sequitur nonsense with Isabelle when warnings appear before proofstate. (da, 1hr?) @@ -377,6 +382,13 @@ B CRUCIAL: Do something to manage .thy and .ML files coherently. (Probably answer: Isabelle needs to support non-automatic reading of ML file: a function "use_thy_only" ). +B (part of above): Handle proof-retract-file by querying Isabelle + about the decendants of a file. Then all the descendents can + also be unlocked. + +X Splash screen: Add fancy text logo to it. Centre the display + prettily. + X Write perl scripts to generate TAGS file for ML and thy files. (6h, I've completely forgotten perl), or better: -- cgit v1.2.3