More comments on current bugs

1 files changed, 16 insertions, 2 deletions

diff --git a/etc/isar/XSymbolTests.thy b/etc/isar/XSymbolTests.thy
index 7402ed81..c1f2a976 100644
--- a/etc/isar/XSymbolTests.thy
+++ b/etc/isar/XSymbolTests.thy
@@ -4,11 +4,21 @@
 
 theory XSymbolTests = Main:
 
+(* At the moment, electric token input doesn't work
+despite being enabled.  So writing a token 
+like  \<alpha> doesn't immediately replace it. *)
+
 constdefs
  P1 :: bool   ("P\<^sub>1")    (* subscript *)
  "P\<^sub>1 == True"
 
-theorem "P\<^sub>1";    (* check subscript appears in goals window *)
+(* Buglet here: if we enable x-sym during scripting,
+   goals/response flks are not updated, so subscripts
+   do not appear in output windows.  
+   Restarting prover fixes.
+*)
+
+theorem "P\<^sub>1";  (* check subscript appears in goals window *)
 by (simp add: P1_def)  (* .. and response window *)
 
 consts
@@ -16,13 +26,17 @@ consts
  "\<^bold>X"  :: bool   (* bold character *)
 
 
+(* Markus reports that · is saved in the file as
+an 8-bit character.  I can't repeat that with XEmacs 21.4,
+unless I set the relevant X-Symbol menu option. *)
 
 (* 
  Another X-Symbol oddity: sometimes the _first_ buffer to
- be visited displays _some_ characters wrongly, e.g. \234 
+ be visited displays _some_ characters as \2xx, e.g.
  for \<circ>.  But subsequent buffers to be visited work
  fine.  Problem is stable for turning x-symbol on/off.
  Revisting the first buffer cures the problem.
+ I can't easily repeat the problem...
 *)
 
 consts