isar/todo


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29

-*- mode:outline -*-

* Things to do for Isabelle/Isar

See also ../todo for generic things to do, priority codes.

** B Isabelle support for ML and legacy files: would like to remove "isa" instance
     Could we handle theory files and even allow scripting in ML files
     at the same time as Isar?  Maybe not, if this is even beyond what
     Isar interface would allow (unless we send an ML file
     line-by-line with ML_command?)

** B theorem dependencies: using Isar's "thm" command does not
   work at top level.  This is annoying for browsing the fully
   qualified dependency names.  (Even the ML_command "thm"
   returns unknown theory context error).  Can we use something
   else?

** B visualise dependencies: sometimes not applicable.

** C func-menu: 
	observe proof-syntactic-context (general problem of func-menu setup?);

** C undo 'use' command: unlock corresponding ML file;

** C provide template for empty theory (or even just for Scratch.thy);

** C proper proof-by-pointing support (hard; needs major reworking of
     Isabelle's pretty-printing subsystem);