Opened 17 years ago

Closed 16 years ago

#112 closed defect (fixed)

Filter out control characters in shell buffer or copy from shell buffer

Reported by: David Aspinall Owned by: David Aspinall
Priority: major Milestone: PG-Emacs-3.7
Component: 2:pg-emacs Keywords:
Cc:

Description (last modified by David Aspinall)

Any idea how I can get rid of the characters such as Ú that appear in the Isabelle shell buffer? XEmacs doesn't display them, but they appear if printed or pasted into other text files. 

+++    ~(c_BT_Obt_OLf t_a = c_BT_Obt_OLf t_a)Û
Ú+++ INFERENCE: Equality
+++ {lit = ~(c_BT_Obt_OLf t_a = c_BT_Oreflect t_a (c_BT_Obt_OLf t_a)),
+++  path = [1], res = c_BT_Obt_OLf t_a, lr = true, thm = |- F}Û
Ú+++   isa th: "False"  [.]Û
Ú+++ fol_term_to_hol: c_BT_Obt_OLf t_a = c_BT_Oreflect t_a (c_BT_Obt_OLf t_a)Û
Ú+++   result type: boolÛ
Ú

Change History (3)

comment:1 Changed 17 years ago by David Aspinall

Description: modified (diff)

comment:2 Changed 17 years ago by David Aspinall

Component: 1:pg-eclipse → 2:pg-emacs

comment:3 Changed 16 years ago by Proof General Developer

Resolution: → fixed
Status: new → closed

Now fixed (in proof-shell.el) by cleaning up the output after it's been processed.

Note: See TracTickets for help on using tickets.