diff options
| -rw-r--r-- | isa/ProofGeneral.ML | 28 | ||||
| -rw-r--r-- | isa/isa.el | 14 |
2 files changed, 29 insertions, 13 deletions
diff --git a/isa/ProofGeneral.ML b/isa/ProofGeneral.ML index 23719994..293eac39 100644 --- a/isa/ProofGeneral.ML +++ b/isa/ProofGeneral.ML @@ -19,7 +19,7 @@ sig (* Processing used files *) - val retract_ML_file : string -> unit + val retract_ML_files_children : string -> unit val retract_thy_file : string -> unit val list_loaded_files : unit -> unit val restart : unit -> unit @@ -27,6 +27,7 @@ sig val update : unit -> unit (* not used *) + val retract_ML_file : string -> unit val use_thy_and_update : string -> unit (* visible only for testing *) @@ -157,19 +158,20 @@ structure ProofGeneral : PROOFGENERAL = (* subroutine: retract a file and give message, if it hasn't been already reported to Proof General. *) - fun retract_file_and_give_message filename = + fun retract_file_and_give_message filename msg_flag = if filename="" orelse (filename mem !retracted_files) then () - else (retract_msg filename; + else (if msg_flag then (retract_msg filename) else (); retracted_files := filename :: !retracted_files; ()) - fun retract_file1 not_thy filename = + fun retract_file1 not_thy only_report_children filename = let val (path, tname) = split_filename filename fun show_msgs thy = let val (thy_file, ml_file) = get_thy_filenames (path_of thy) thy in (if not_thy then () - else retract_file_and_give_message thy_file; - retract_file_and_give_message ml_file) end + else retract_file_and_give_message thy_file true; + retract_file_and_give_message ml_file + (not only_report_children)) end (* Considered loaded if either theory or ML times set *) fun already_loaded thy = let val t = get_thyinfo thy @@ -185,18 +187,24 @@ structure ProofGeneral : PROOFGENERAL = in if already_loaded tname then (show_msgs tname; - map (retract_file1 false) (children_loaded tname); ()) + map (retract_file1 false false) (children_loaded tname); ()) else () end; (* retract a script file and all it's theory/script children, - but not it's parent theory. *) + but not it's parent theory. *) + + val retract_ML_file = retract_file1 true false; + + (* Same as above, but only give reports to Proof General for + the children. *) + + val retract_ML_files_children = retract_file1 true true; - val retract_ML_file = retract_file1 true; (* retract a theory file and all it's theory/script children *) - val retract_thy_file = retract_file1 false; + val retract_thy_file = retract_file1 false false; (* USING files. @@ -387,6 +387,12 @@ Resulting output from Isabelle will be parsed by Proof General." :type 'string :group 'isabelle-config) +(defcustom isa-retract-ML-files-children-command "ProofGeneral.retract_ML_files_children \"%s\";" + "Sent to Isabelle to forget the descendants of an ML file. +Resulting output from Isabelle will be parsed by Proof General." + :type 'string + :group 'isabelle-config) + (defun isa-retract-thy-file (file) "Retract the theory file FILE. If interactive, use buffer-file-name." (interactive (list buffer-file-name)) @@ -501,15 +507,17 @@ Resulting output from Isabelle will be parsed by Proof General." (defun isa-find-and-forget (span) "Return a command to be used to forget SPAN." (save-excursion + ;; FIXME: bug here: too much gets retracted. ;; See if we are going to part way through a completely processed ;; buffer, in which case it should be removed from ;; proof-included-files-list along with any other buffers - ;; depending on it. NB: perhaps this is called too often for - ;; a bunch of spans in a region? + ;; depending on it. However, even though we send the retraction + ;; command to Isabelle we don't want to *completely* unlock + ;; the current buffer. How can this be avoided? (goto-char (point-max)) (skip-chars-backward " \t\n") (if (>= (proof-unprocessed-begin) (point)) - (format isa-retract-ML-file-command + (format isa-retract-ML-files-children-command (file-name-sans-extension (file-name-nondirectory (buffer-file-name)))) |