diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 1998-11-25 12:48:33 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 1998-11-25 12:48:33 +0000 |
| commit | 5870622e827747ffb096225562b4b2599e31c50c (patch) | |
| tree | 6c01076abcb4ed40cfeac5c62812a776eb01b04d /isa/ProofGeneral.ML | |
| parent | f1e1e37ac85ab5f6746d03b067628605fb67ab09 (diff) | |
Added Isamode-like keybinding C-c C-l for proof-prf.
Diffstat (limited to 'isa/ProofGeneral.ML')
| -rw-r--r-- | isa/ProofGeneral.ML | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/isa/ProofGeneral.ML b/isa/ProofGeneral.ML index 1663953d..0e5eace5 100644 --- a/isa/ProofGeneral.ML +++ b/isa/ProofGeneral.ML @@ -377,10 +377,10 @@ in fun print_current_goals_with_plain_output i j t = Library.setmp prs_fn out (print_current_goals_default i j) t; - (* Annoyingly, Proof General waits for the first prompt before doing - anything. Hack sending a prompt to get things going *) +(* Annoyingly, Proof General waits for the first prompt before doing + anything. Hack sending a prompt to get things going *) - val _ = out "> \n"; + val _ = out ">\250 \n"; end; print_current_goals_fn := print_current_goals_with_plain_output; @@ -388,9 +388,11 @@ print_current_goals_fn := print_current_goals_with_plain_output; (* add specials to ml prompts *) +ml_prompts ">\250" "-\251"; (* ?\372, ?\373 *) + + + (* - ml_prompts ">\250" "-\251"; (* ?\372, ?\373 *) - NB: Obscure bug with proof-shell-annotated-prompt-regexp set properly to include annotations: PG doesn't recognize first proof state output. |