Commit a71bb6da authored by Heiko Becker's avatar Heiko Becker

Add keyxbinding to backtrack proof (C-c C-u) and remove dependency for IEEE by...

Add keyxbinding to backtrack proof (C-c C-u) and remove dependency for IEEE by commenting out and add show_type function
parent d5b6ccb8
......@@ -28,17 +28,11 @@ echo "DO NOT CHANGE THIS FILE! IF CHANGES ARE NECESSARY ADD THEM TO THE configur
echo "*)" >> .ocamlinit
echo "#cd \""$HOLLIGHT_HOME"\";;" >> .ocamlinit
echo "#use \"hol.ml\";;" >> .ocamlinit
echo "#use \"./IEEE/make.ml\";;" >> .ocamlinit
#if [ ! -z "$PG_DIR" ]
#then
# echo "#cd \""$PG_DIR"\";;" >>.ocamlinit
# echo "#use \"pg_prompt.ml\";;" >>.ocamlinit
# echo "#use \"pg_tactics.ml\";;" >>.ocamlinit
#fi
#echo "#use \"./IEEE/make.ml\";;" >> .ocamlinit
echo "#cd \""$CURR_DIR"\";;" >>.ocamlinit
echo "#use \"Tactician/main.ml\";;" >> .ocamlinit
echo "#use \"Infra/types.ml\";;" >>.ocamlinit
# Setup dmtcp
if [ -z `command -v dmtcp_launch >/dev/null 2>&1` ]
......
......@@ -950,6 +950,7 @@ Regexp match data 0 points to the chars."
(define-key map "\C-c\C-k" 'hol-light-kill-caml)
(define-key map "\C-c\C-n" 'hol-light-next-phrase)
(define-key map "\C-c\C-p" 'hol-light-previous-phrase)
(define-key map "\C-c\C-u" 'hol-light-send-backtrack)
(define-key map [(control c) (home)] 'hol-light-move-inside-block-opening)
(define-key map [(control c) (control down)] 'hol-light-next-phrase)
(define-key map [(control c) (control up)] 'hol-light-previous-phrase)
......@@ -2968,6 +2969,19 @@ current phrase else insert a newline and indent."
(let ((pair (hol-light-discover-phrase)))
(narrow-to-region (nth 0 pair) (nth 1 pair)))))
(defun hol-light-send-backtrack ()
"Send a backtrack command to the HOL-Light interactive session."
(interactive)
(newline)
(setq curr-line (line-number-at-pos))
(insert " b();;")
(newline)
(goto-line curr-line)
(hol-light-eval-phrase)
(goto-line curr-line)
(kill-line 1)
(delete-backward-char 1))
(defun hol-light-eval-phrase ()
"Eval the surrounding Caml phrase (or block) in the Caml toplevel."
(interactive)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment