experiments with theorem dependencies

2 files changed, 9 insertions, 4 deletions

diff --git a/isa/depends.ML b/isa/depends.ML
index a8b45d2c..d55b7552 100644
--- a/isa/depends.ML
+++ b/isa/depends.ML
@@ -60,12 +60,12 @@ fun thm_deps thms =
 
 fun new_thm_deps thms =
   let
-    val _ = print "Proof General, the theorem dependencies are:   ";
+    val header = "Proof General, the theorem dependencies are: \"";
     val gra = map snd (Symtab.dest (fst (foldl make_deps_graph ((Symtab.empty, []),
       map (#der o rep_thm) thms))));
-    fun printname s = (print s; print " ");
-    val _ = seq printname (foldl (op@) ([],(map #parents gra)));
-  in writeln "" end;
+    val deps = foldl (op@) ([],(map #parents gra))
+    val msg = header ^ (space_implode " " deps) ^ "\""
+  in writeln msg end;
 
 val old_qed = qed;
 
diff --git a/isa/isa.el b/isa/isa.el
index 642dcc13..3eca01bf 100644
--- a/isa/isa.el
+++ b/isa/isa.el
@@ -211,6 +211,11 @@ and script mode."
    ;; Some messages delimited by eager annotations
    proof-shell-clear-response-regexp    "Proof General, please clear the response buffer."
    proof-shell-clear-goals-regexp       "Proof General, please clear the goals buffer."
+   (setq proof-shell-theorem-dependency-list-regexp    "Proof General, the theorem dependencies are: \"\\([^\"]*\\)\"") 
+   
+   ;; FIONA! Add something here to set 
+   ;; proof-shell-theorem-dependency-list-regexp
+   ;; to something to match from Isabelle output
 
    ;; Dirty hack to allow font-locking for output based on hidden
    ;; annotations, see isa-output-font-lock-keywords-1