diff options
| -rw-r--r-- | isa/ProofGeneral.ML | 109 | ||||
| -rw-r--r-- | isa/isa.el | 49 | ||||
| -rw-r--r-- | isa/thy-mode.el | 7 |
3 files changed, 158 insertions, 7 deletions
diff --git a/isa/ProofGeneral.ML b/isa/ProofGeneral.ML index c47d11c4..8f617665 100644 --- a/isa/ProofGeneral.ML +++ b/isa/ProofGeneral.ML @@ -180,4 +180,111 @@ structure ProofGeneral = fun show_context () = the_context(); end; -
\ No newline at end of file + +(* duplicated code from thy_read.ML *) + +val tmp_loadpath = ref [] : string list ref; + +fun find_file "" name = + let fun find_it (cur :: paths) = + if File.exists (tack_on cur name) then + (if cur = "." then name else tack_on cur name) + else + find_it paths + | find_it [] = "" + in find_it (!tmp_loadpath @ !loadpath) end + | find_file path name = + if File.exists (tack_on path name) then tack_on path 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"); + val absolute_path = absolute_path (OS.FileSys.getDir ()); + val thy_file = absolute_path found; + val (thy_path, _) = split_filename thy_file; + val found = find_file path (name ^ ".ML"); + val ml_file = if thy_file = "" then absolute_path found + else if File.exists (tack_on thy_path (name ^ ".ML")) + then tack_on thy_path (name ^ ".ML") + else ""; + val searched_dirs = if path = "" then (!tmp_loadpath @ !loadpath) + else [path] + in if thy_file = "" andalso ml_file = "" then + (* Proof General change: only give warning message here *) + warning ("Could not find file \"" ^ name ^ ".thy\" or \"" + ^ name ^ ".ML\" for theory \"" ^ name ^ "\"\n" + ^ "in the following directories: \"" ^ + (space_implode "\", \"" searched_dirs) ^ "\"") + else (); + (thy_file, ml_file) + end; + + val tinfo = get_thyinfo name; + in if is_some tinfo andalso path = "" then + let val {path = abs_path, ...} = the tinfo; + val (thy_file, ml_file) = if abs_path = "" then new_filename () + else (find_file abs_path (name ^ ".thy"), + find_file abs_path (name ^ ".ML")) + in if thy_file = "" andalso ml_file = "" then + (warning ("File \"" ^ (tack_on path name) + ^ ".thy\"\ncontaining theory \"" ^ name + ^ "\" no longer exists."); + new_filename () + ) + else (thy_file, ml_file) + end + else new_filename () + end; + +fun retract_file thy = + let fun file_msg x = if (x <> "") then + writeln ("Proof General, you can unlock the file " + ^ (quote x)) + else () + (* output messages for this theory *) + val (thy_file, ml_file) = get_filenames (path_of thy) thy + val _ = file_msg thy_file + val _ = file_msg ml_file + (* now process this theory's children *) + val children = children_of thy; + val present = filter (is_some o get_thyinfo) children; + fun already_loaded thy = + let val t = get_thyinfo thy + in if is_none t then false + else let val {thy_time, ml_time, ...} = the t + in is_some thy_time andalso is_some ml_time end + end + val loaded = filter already_loaded present; + in + if loaded <> [] then + (map retract_file loaded; ()) + else () + end; + +fun list_loaded_files () = + let + 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 + fun file_msg x = if (x <> "") then + (* Simulate output of theory loader *) + writeln ("Reading " ^ (quote x)) + else () + in + (file_msg thy_file; file_msg ml_file) + end + in + seq loading_msg thys_list + end; + +(* Get Proof General to cache the loaded files. *) + +list_loaded_files(); + + + + + @@ -120,7 +120,7 @@ no regular or easily discernable structure." "use \"" proof-internal-home-directory "isa/ProofGeneral.ML\";") - proof-shell-eager-annotation-start "^\\[opening \\|^###" + proof-shell-eager-annotation-start "^\\[opening \\|^###\\|^Reading\\|^Proof General" proof-shell-eager-annotation-end "$" ;; === ANNOTATIONS === ones below here are broken proof-shell-goal-char ?\375 @@ -130,7 +130,27 @@ no regular or easily discernable structure." proof-analyse-using-stack t proof-shell-start-char ?\372 proof-shell-end-char ?\373 - proof-shell-field-char ?\374)) + proof-shell-field-char ?\374 + ;; NEW NEW for multiple files + ;; === NEW NEW: multiple file stuff. move elsewhere later. + proof-shell-process-file + (cons + ;; Theory loader output + "Reading \"\\(.*\\.ML\\)\"" + (lambda (str) + (match-string 1 str))) + ;; This is the output returned by a special command to + ;; query Isabelle for outdated files. + proof-shell-retract-files-regexp + "Proof General, you can unlock the file \"\\(.*\\)\"" + proof-shell-compute-new-files-list 'isa-shell-compute-new-files-list + )) + +(defun isa-shell-compute-new-files-list (str) + (assert (member (file-truename (match-string 1 str)) + proof-included-files-list)) + (remove (file-truename (match-string 1 str)) + proof-included-files-list)) ;; ===== outline mode @@ -253,11 +273,28 @@ isa-proofscript-mode." ;; backwards in isa-find-and-forget, rather than forwards as ;; the old code below does. +(defconst isa-retract-file-command "retract_file \"%s\";" + "Command sent to Isabelle for forgetting") + (defun isa-find-and-forget (span) - ;; Special return value to indicate nothing needs to be done. - proof-no-command) - - + ;; See if we are going to part way through a completely processed + ;; buffer. + (if (eq (current-buffer) (car-safe proof-script-buffer-list)) + ;; Special return value to indicate nothing needs to be done. + proof-no-command + (progn + (save-excursion + (goto-char (point-max)) + (skip-chars-backward "\\S-") + (if (member (proof-unprocessed-begin) (list (point-min) (point))) + ;; + (format isa-retract-file-command + (file-name-sans-extension + (file-name-nondirectory + (buffer-file-name)))) + prog-no-command))))) + + ;; BEGIN Old code (taken from Coq.el) ;(defconst isa-keywords-decl-defn-regexp ; (ids-to-regexp (append isa-keywords-decl isa-keywords-defn)) diff --git a/isa/thy-mode.el b/isa/thy-mode.el index 4a53bf29..a9690394 100644 --- a/isa/thy-mode.el +++ b/isa/thy-mode.el @@ -176,6 +176,7 @@ The style of indentation for theory files is controlled by these variables: (setq mode-name "Theory") (use-local-map thy-mode-map) ;; (isa-menus) ; Add "isabelle" menu. + (set-syntax-table thy-mode-syntax-table) (make-local-variable 'indent-line-function) (setq indent-line-function 'thy-indent-line) @@ -186,6 +187,12 @@ The style of indentation for theory files is controlled by these variables: (setq comment-start-skip "(\\*+[ \t]?") ; . (setq font-lock-keywords thy-mode-font-lock-keywords) + + ;; Toolbar: needs alteration for non-scripting mode! + ;; (if (featurep 'proof-toolbar) + ;; (proof-toolbar-setup)) + ;; + (run-hooks 'thy-mode-hook) (force-mode-line-update) (if (null nomessage) |