Custom Query (361 matches)
Results (31 - 33 of 361)
| Ticket | Resolution | Summary | Owner | Reporter |
|---|---|---|---|---|
| #112 | fixed | Filter out control characters in shell buffer or copy from shell buffer | ||
| Description |
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Û
Ú
|
|||
| #113 | fixed | Coq commands not described in coq/coq-syntax.el | ||
| Description |
Hello, The following commands, given in the "Vernacular Commands Index" in Coq Reference Manual are not listed in coq-commands-db in coq/coq-syntax.el. As a result, they are not highlighted and, more importantly, they are though to be not state preserving and so are not executed by proof-minibuffer-cmd command. About Pwd Search Test The "Check" command is mentioned but it is marked as not state preserving as well. Could you change this? Thank you, Yevgeniy |
|||
| #114 | fixed | Spurious "replaced xyz occurrences" messages | ||
| Description |
I keep getting "Replaced xyz occurrences" in the xemacs minibuffer after each PG interaction, where xyz depends on the length of the text. As Makarius said, we don't think it is a PG but an xemacs thing. But since you asked me to put it here... Clemens seems to be using the same setup but gets no such message. I started getting it after updating my MAC OS and my xemacs to [version 21.4.20; April 2007]. Tobias |
|||
