diff options
Diffstat (limited to 'hol-light/pg_prompt.ml')
| -rw-r--r-- | hol-light/pg_prompt.ml | 41 |
1 files changed, 41 insertions, 0 deletions
diff --git a/hol-light/pg_prompt.ml b/hol-light/pg_prompt.ml new file mode 100644 index 00000000..f52dc76e --- /dev/null +++ b/hol-light/pg_prompt.ml @@ -0,0 +1,41 @@ +(* ========================================================================= *) +(* HOL Light tweaks for Proof General. *) +(* *) +(* Mark Adams, David Aspinall. *) +(* LFCS, School of Informatics, University of Edinburgh *) +(* *) +(* (c) Copyright University of Edinburgh and authors, 2012. *) +(* *) +(* This file adjust the OCaml prompt to help Proof General synchronization. *) +(* It is loaded before HOL Light. *) +(* ========================================================================= *) + + +(* ------------------------------------------------------------------------- *) +(* Proof General mode, providing extra annotations in output *) +(* ------------------------------------------------------------------------- *) + +let pg_mode = ref (true : bool);; + +let pg_mode_on () = (pg_mode := true);; +let pg_mode_off () = (pg_mode := false);; + +let pg_prompt_info = ref (fun () -> "");; + + +(* ------------------------------------------------------------------------- *) +(* Adjust the OCaml prompt to carry information for Proof General. *) +(* ------------------------------------------------------------------------- *) + +let original_prompt_fn = !Toploop.read_interactive_input in +(Toploop.read_interactive_input := + fun prompt buffer len -> + let prompt' = + if (!pg_mode) + then "<prompt>" ^ + (!pg_prompt_info()) ^ + "</prompt>" + else prompt in + original_prompt_fn prompt' buffer len);; + + |