Begun work on adding more special annotations for Isabelle.

2 files changed, 54 insertions, 41 deletions

diff --git a/isa/ProofGeneral.ML b/isa/ProofGeneral.ML
index 2ed9af59..acfaf755 100644
--- a/isa/ProofGeneral.ML
+++ b/isa/ProofGeneral.ML
@@ -117,40 +117,53 @@ fun use_thy_and_update thy = (use_thy_no_topml thy; update(); list_loaded_files(
 
 (* configure output channels to decorate output *)
 
-(*
- Frustratingly, Isabelle uses prs_fn also when displaying
- the goal state, so it's no use setting that hoping to catch
- all "normal" output separately.  We really need a fourth
- output channel.
- *)
-	       
 local
   fun out s =
     (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut);
 
-  fun prefix_suffix_lines prfx txt sufx  =
-    txt |> split_lines |> map (fn s => prfx ^ s ^ sufx ^ "\n") |> implode;
+  fun prefix_lines prfx txt =
+    txt |> split_lines |> map (fn s => prfx ^ s ^ "\n") |> implode;
 in
+    (* \240 is octal 360, first special character used. *)
     val _ =
-      (* No difference to original functions at the moment. *)
-      (prs_fn := (fn s => out s) ;
-       warning_fn :=  (fn s => out (prefix_suffix_lines "### " s "")) ;
-       error_fn := (fn s => out (prefix_suffix_lines "*** " s "")))
+      (prs_fn := 
+	   (fn s => out ("\240" ^ s ^ "\241"));
+       warning_fn :=
+	   (fn s => out ("\242" ^ (prefix_lines "###" s) ^ "\243"));
+       error_fn :=
+	   (fn s => out ("\244" ^ (prefix_lines "###" s) ^ "\245")))
 end;
 
-      
+(* add specials to ml prompts *)
 
+ml_prompts "\250>" "\251-";  (* ?\372, ?\373 *)
 
 (* add markup to proof state output *)
 
-val proof_state_special_prefix="\248";  (* \370 octal *)
-val proof_state_special_suffix="\249";  (* \371 *)
-val goal_start_special="\253";	        (* \375 *)
+val proof_state_special_prefix="\246";  (* ?\366 *)
+val proof_state_special_suffix="\247";  (* ?\367 *)
+val goal_start_special="\248";	        (* ?\370 *)
 
 current_goals_markers:=(proof_state_special_prefix,
 			proof_state_special_suffix,
 		        goal_start_special);
 
+local
+  fun out s =
+    (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut);
+in
+    fun print_current_goals_with_plain_output i j t =
+  let
+    val curr_prs = !prs_fn
+    val _ = prs_fn := (fn s => out s)
+    val _ = (print_current_goals_default i j t)
+		handle e => (prs_fn := curr_prs; raise e)
+  in       
+    prs_fn := curr_prs
+  end
+end;
+
+print_current_goals_fn := print_current_goals_with_plain_output;
 
 
 (* Turn on verbose update output, Proof General likes to parse it.
diff --git a/isa/isa.el b/isa/isa.el
index 5610c666..ea5d33f0 100644
--- a/isa/isa.el
+++ b/isa/isa.el
@@ -71,11 +71,6 @@ no regular or easily discernable structure."
 ;;; End of a command needs parsing to find, so this is approximate.
 (defvar isa-outline-heading-end-regexp ";[ \t\n]*")
 
-(defconst isa-goal-regexp "^[ \t]*[0-9]+\\. "
-  "Regexp to match subgoal headings.
-Used by proof mode to parse proofstate output, and also
-to set outline heading regexp.")
-  
 ;; 
 (defvar isa-shell-outline-regexp isa-goal-regexp)
 (defvar isa-shell-outline-heading-end-regexp isa-goal-regexp)
@@ -134,8 +129,8 @@ to set outline heading regexp.")
    ;; Probably it isn't general enough for all MLs, please send me
    ;; problem reports / patches.
    ;;
-   proof-shell-annotated-prompt-regexp
-					"^\\(val it = () : unit\n\\)?> "
+   proof-shell-annotated-prompt-regexp  "\372>"
+   ;; non annotation, with val it's: "^\\(val it = () : unit\n\\)?> "
 
    ;; This pattern is just for comint, it matches a range of
    ;; prompts from a range of MLs.
@@ -146,26 +141,31 @@ to set outline heading regexp.")
    ;; FIXME: the next two are probably only good for NJ/SML
    proof-shell-error-regexp		"^.*Error:\\|^\\*\\*\\*"
    proof-shell-interrupt-regexp         "Interrupt"
-   ;; this one not set: proof-shell-abort-goal-regexp 
-   proof-shell-noise-regexp	        ""
-   proof-shell-assumption-regexp	isa-id  ; matches name of assumptions
-   proof-shell-goal-regexp		isa-goal-regexp    ; matches subgoal heading
-   ;; FIXME: hack the SML prompt using ml_prompt and set wakeup-char.
-   proof-shell-wakeup-char		nil
-   proof-shell-start-goals-regexp	"\370"
-   proof-shell-end-goals-regexp		"\371"
+   
+   ;; nothing appropriate for: proof-shell-abort-goal-regexp
+   ;; proof-shell-noise-regexp isn't used anywhere at the moment.
+   proof-shell-noise-regexp	        "val it = () : unit\n"
+   ;; matches names of assumptions
+   proof-shell-assumption-regexp	isa-id
+   ;; matches subgoal name
+   proof-shell-goal-regexp		"\370[ \t]*\\([0-9]+\\)\\."
+
+   proof-shell-wakeup-char		?\372
+   proof-shell-start-goals-regexp	"\366"
+   proof-shell-end-goals-regexp		"\367"
+   proof-shell-goal-char	        ?\370
    ;; initial command configures Isabelle by hacking print functions.
-   ;; may need to set directory somewhere for this:
-   ;; /home/da/devel/lego/elisp/   or  $PROOFGENERIC_HOME ?
-   proof-shell-init-cmd			(concat
-					 "use \""
-					 proof-home-directory
-					  "isa/ProofGeneral.ML\";")
-   proof-shell-eager-annotation-start   "^\\[opening \\|^###\\|^Reading\\|^Proof General\\|^Not reading"  ; "^---\\|^\\[opening "
+   proof-shell-init-cmd
+     (concat "use \"" proof-home-directory "isa/ProofGeneral.ML\";")
+   proof-shell-eager-annotation-start   "\360\\|\362\\|\364"
+   proof-shell-eager-annotation-end     "\361\\|\363\\|\365"
+
+   ;; Tested values of proof-shell-eager-annotation-start: 
+   ;; "^\\[opening \\|^###\\|^Reading\\|^Proof General\\|^Not reading"
+   ;; "^---\\|^\\[opening "
    ;; could be last bracket on end of line, or with ### and ***.
-   proof-shell-eager-annotation-end     "\n"
+
    ;; === ANNOTATIONS  === ones below here are broken
-   proof-shell-goal-char	        ?\375
    proof-shell-first-special-char	?\360
    proof-shell-result-start	        "\372 Pbp result \373"
    proof-shell-result-end		"\372 End Pbp result \373"