diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 1998-10-21 10:10:13 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 1998-10-21 10:10:13 +0000 |
| commit | b8cd86cd4c7dc8ada21566482c95016f50f6e617 (patch) | |
| tree | dad03ec75d9648945f8c6a585662b721c0441591 /isa/ProofGeneral.ML | |
| parent | 0ecbb5c7c13442f2135ae5972592e17dcb7ef02e (diff) | |
Used new get_thy_filenames function from Isabelle 98-1
Diffstat (limited to 'isa/ProofGeneral.ML')
| -rw-r--r-- | isa/ProofGeneral.ML | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/isa/ProofGeneral.ML b/isa/ProofGeneral.ML index 8f617665..586d5992 100644 --- a/isa/ProofGeneral.ML +++ b/isa/ProofGeneral.ML @@ -198,6 +198,7 @@ fun find_file "" name = else ""; (*Get absolute pathnames for a new or already loaded theory *) +(* fun get_filenames path name = let fun new_filename () = let val found = find_file path (name ^ ".thy"); @@ -237,6 +238,9 @@ fun get_filenames path name = end else new_filename () end; +Not needed in latest version of Isabelle with my hack. +*) + fun retract_file thy = let fun file_msg x = if (x <> "") then @@ -244,7 +248,7 @@ fun retract_file thy = ^ (quote x)) else () (* output messages for this theory *) - val (thy_file, ml_file) = get_filenames (path_of thy) thy + val (thy_file, ml_file) = get_thy_filenames (path_of thy) thy val _ = file_msg thy_file val _ = file_msg ml_file (* now process this theory's children *) @@ -268,7 +272,7 @@ fun list_loaded_files () = val thys_list = Symtab.dest (!loaded_thys) fun loading_msg (tname,tinfo) = let val path = path_of tname - val (thy_file,ml_file) = get_filenames path tname + val (thy_file,ml_file) = get_thy_filenames path tname fun file_msg x = if (x <> "") then (* Simulate output of theory loader *) writeln ("Reading " ^ (quote x)) |