Merge changes from Version4Branch.

9 files changed, 633 insertions, 1276 deletions

diff --git a/isar/Example-Tokens.thy b/isar/Example-Tokens.thy
new file mode 100644
index 00000000..2eee4f18
--- /dev/null
+++ b/isar/Example-Tokens.thy
@@ -0,0 +1,34 @@
+(*
+      Example proof document for Isabelle/Isar Proof General,
+      using symbols.  
+      View and process this document with Unicode Tokens engaged.
+   
+      $Id$
+*)
+
+theory "Example-Xsym" imports Main begin
+
+text {* Proper proof text -- \<^bitalic>naive version\<^eitalic>. *}
+
+theorem and_comms: "\<phi> \<and> \<psi> \<longrightarrow> \<psi> \<and> \<phi>"
+proof
+   assume "\<phi> \<and> \<psi>"
+  then show "\<psi> \<and> \<phi>"
+  proof
+    assume \<psi> and \<phi>
+    then show ?thesis ..
+ qed
+qed
+
+text {* \<^bbold>Unstructured\<^ebold> proof script. *}
+
+theorem "\<phi>\<^isub>\<alpha> \<and> \<phi>\<^isub>\<beta> \<longrightarrow> (\<phi>\<^isub>\<beta>  ∧  \<phi>\<^isub>\<alpha>)"
+  apply (rule impI)
+  apply (erule conjE)
+  apply (rule conjI)
+  apply assumption
+  apply assumption
+done
+
+end
+
diff --git a/isar/Example-Xsym.thy b/isar/Example-Xsym.thy
deleted file mode 100644
index b864428f..00000000
--- a/isar/Example-Xsym.thy
+++ /dev/null
@@ -1,42 +0,0 @@
-(*
-      Example proof document for Isabelle/Isar Proof General.
-   
-      $Id$
-*)
-
-theory "Example-Xsym" imports Main begin
-
-text {* Proper proof text -- \textit{naive version}. *}
-
-theorem and_comms: "A \<and> B \<longrightarrow> B \<and> A"
-proof
-  assume "A \<and> B"
-  then show "B \<and> A"
-  proof
-    assume B and A
-    then show ?thesis ..
- qed
-qed
-
-
-text {* Proper proof text -- \textit{advanced version}. *}
-
-theorem "A \<and> B \<longrightarrow> B \<and> A"
-proof
-  assume "A \<and> B"
-  then obtain B and A ..
-  then show "B \<and> A" ..
-qed
-
-
-text {* Unstructured proof script. *}
-
-theorem "A \<and> B \<longrightarrow> B \<and> A"
-  apply (rule impI)
-  apply (erule conjE)
-  apply (rule conjI)
-  apply assumption
-  apply assumption
-done
-
-end
diff --git a/isar/Example.thy b/isar/Example.thy
index 0fe43c25..e869364b 100644
--- a/isar/Example.thy
+++ b/isar/Example.thy
@@ -24,7 +24,7 @@ theorem "A & B --> B & A"
 proof
   assume "A & B"
   then obtain B and A ..
-  then show "B & A" ..
+  then show "B & A" .. 
 qed
 
 
diff --git a/isar/interface-setup.el b/isar/interface-setup.el
index d6ea1341..effb3541 100644
--- a/isar/interface-setup.el
+++ b/isar/interface-setup.el
@@ -11,19 +11,14 @@
 ;;
 
 ;;
-;; X-Symbol
+;; X-Symbol -- backwards compatibility
 ;;
 
 (let ((xsymbol (getenv "PROOFGENERAL_XSYMBOL")))
 
-  ;; avoid confusing warning message
-  (if (not (boundp 'x-symbol-image-converter))     
-      (customize-set-variable 'x-symbol-image-converter nil))
-  
   ;; tell Proof General about -x option
   (if (and xsymbol (not (equal xsymbol "")))
-      (customize-set-variable 'isar-x-symbol-enable (equal xsymbol "true"))))
-
+      (customize-set-variable 'isar-unicode-tokens-enable (equal xsymbol "true"))))
 
 ;;
 ;; Unicode
diff --git a/isar/isabelle-system.el b/isar/isabelle-system.el
index 538d18e9..4f39fc44 100644
--- a/isar/isabelle-system.el
+++ b/isar/isabelle-system.el
@@ -29,8 +29,6 @@
 
 (defcustom isabelle-web-page
   "http://www.cl.cam.ac.uk/Research/HVG/Isabelle/"
-  ;; "http://isabelle.in.tum.de"
-  ;; "http://www.dcs.ed.ac.uk/home/isabelle"
   "URL of web page for Isabelle."
   :type 'string
   :group 'isabelle)
@@ -59,18 +57,18 @@ working."
 (defvar isatool-not-found nil
   "Non-nil if user has been prompted for `isatool' already and it wasn't found.")
 
-(defun isa-set-isatool-command ()
+(defun isa-set-isatool-command (&optional force)
   "Make sure isa-isatool-command points to a valid executable.
-If it does not, prompt the user for the proper setting.
-If it appears we're running on win32 or FSF Emacs, we allow this to
-remain unverified.
-Returns non-nil if isa-isatool-command is surely an executable
-with full path."
-  (interactive)
-  (unless (or noninteractive
-	      proof-rsh-command 
-	      isatool-not-found 
-	      (file-executable-p isa-isatool-command))
+If it does not, or if prefix arg supplied, prompt the user for
+the proper setting.  If `proof-rsh-command' is set, leave this
+unverified.  Otherwise, returns non-nil if isa-isatool-command 
+is surely an executable with full path."
+  (interactive "p")
+  (when (and (not noninteractive)
+	     (not proof-rsh-command)
+	     (or force 
+		 isatool-not-found 
+		 (not (file-executable-p isa-isatool-command))))
     (setq isa-isatool-command
 	  (read-file-name
 	   "Please give the full path to `isatool' (RET if you don't have it): "
@@ -159,6 +157,7 @@ at the top of your theory file, like this:
 	 (list '(string :tag "Choose another")
 	       '(const :tag "Unset (use default)" nil)))
   :group 'isabelle)
+(put 'isabelle-chosen-logic 'safe-local-variable 'stringp)
 
 (defvar isabelle-chosen-logic-prev nil
   "Value of `isabelle-chosen-logic' on last call of `isabelle-set-prog-name'.")
@@ -291,12 +290,14 @@ for you, you should disable this behaviour."
 		  (isabelle-choose-logic nil)
 		  :active (not (proof-shell-live-buffer))
 		  :style radio
-		  :selected (not isabelle-chosen-logic)])
+		  :selected (not isabelle-chosen-logic)
+		  :help "Switch to default logic"])
 	       (mapcar (lambda (l)
 			 (vector l (list 'isabelle-choose-logic l)
 				 :active '(not (proof-shell-live-buffer))
 				 :style 'radio
-				 :selected (list 'equal 'isabelle-chosen-logic l)))
+				 :selected (list 'equal 'isabelle-chosen-logic l)
+				 :help (format "Switch to %s logic" l)))
 		       isabelle-logics-available)))))
 
 (unless noninteractive
@@ -314,38 +315,22 @@ for you, you should disable this behaviour."
       (progn
 	(setq isabelle-logics-available (isa-tool-list-logics))
 	(isabelle-logics-menu-calculate)
-	(if (not (featurep 'xemacs))
-	    ;; update the menu manually
-	    (easy-menu-add-item proof-assistant-menu nil
-				isabelle-logics-menu-entries))
+	;; update the menu manually
+	(easy-menu-add-item proof-assistant-menu nil
+			    isabelle-logics-menu-entries)
 	(setq isabelle-time-to-refresh-logics nil) ;; just done it, don't repeat!
-	(run-with-timer 2 nil ;; short delay to avoid doing this too often
+	(run-with-timer 4 nil ;; short delay to avoid doing this too often
 			(lambda () (setq isabelle-time-to-refresh-logics t))))))
 
-;; Function for XEmacs only
-(defun isabelle-logics-menu-filter (&optional ignored)
-  (isabelle-logics-menu-refresh)
-  (cdr isabelle-logics-menu-entries))
-
-;; Functions for GNU Emacs only to update logics menu
-(if (not (featurep 'xemacs))
 (defun isabelle-menu-bar-update-logics ()
   "Update logics menu."
   (and (current-local-map)
        (keymapp (lookup-key (current-local-map)
  			    (vector 'menu-bar (intern proof-assistant))))
-       (isabelle-logics-menu-refresh))))
-
-(if (not (featurep 'xemacs))
-    (add-hook 'menu-bar-update-hook 'isabelle-menu-bar-update-logics))
+       (isabelle-logics-menu-refresh)))
 
+(add-hook 'menu-bar-update-hook 'isabelle-menu-bar-update-logics)
 
-(defvar isabelle-logics-menu
-   (if (featurep 'xemacs)
-       (cons (car isabelle-logics-menu-entries)
-	     (list :filter 'isabelle-logics-menu-filter)) ;; generates menu on click
-     isabelle-logics-menu-entries)
-  "Isabelle logics menu.  Calculated when Proof General is loaded.")
 
 ;; Added in PG 3.4: load isar-keywords file.
 ;; This roughly follows the method given in the interface script.
@@ -371,37 +356,6 @@ for you, you should disable this behaviour."
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
-;; Generic Isabelle menu for Isabelle and Isabelle/Isar
-;;
-
-(defpgdefault menu-entries
-  isabelle-logics-menu)
-
-(defpgdefault help-menu-entries isabelle-docs-menu)
-
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;
-;; X-Symbol language configuration, and adding to completion table
-;;
-
-(eval-after-load "x-symbol-isar"
-  ;; Add x-symbol tokens to isa-completion-table and rebuild
-  ;; internal completion table if completion is already active
-  '(progn
-     (defpgdefault completion-table
-       (append isar-completion-table
-	       (mapcar (lambda (xsym) (nth 2 xsym))
-		       x-symbol-isar-table)))
-     (setq proof-xsym-font-lock-keywords
-	   x-symbol-isar-font-lock-keywords)
-     (if (featurep 'completion)
-	 (proof-add-completions))))
-
-
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;
 ;; Subterm markup -- faking it
 ;;
 
diff --git a/isar/isar-syntax.el b/isar/isar-syntax.el
index 0dc22392..8c8a4310 100644
--- a/isar/isar-syntax.el
+++ b/isar/isar-syntax.el
@@ -18,43 +18,26 @@
 ;; ----- character syntax
 
 (defconst isar-script-syntax-table-entries
-  (append
-       '(?\$ "."
-         ?\/ "."
-         ?\\ "\\"
-         ?+  "."
-         ?-  "."
-         ?=  "."
-         ?%  "."
-         ?<  "w"
-         ?>  "w"
-         ?\& "."
-         ?.  "w"
-         ?_  "w"
-         ?\' "w"
-         ??  "w"
-         ?`  "\""
-         ?\( "()1"
-         ?\) ")(4")
-   (cond
-    ((featurep 'xemacs)
-     ;; We classify {* sequences *} as comments, although
-     ;; they need to be passed as command args as text.
-     ;; NB: adding a comment sequence b seems to break
-     ;; buffer-syntactic-context, best to use emulated
-     ;; version.
-    '(?\{ "(}5"
-      ?\} "){8"
-      ?\* ". 2367"))
-    ;; previous version confuses the two comment sequences,
-    ;; but works with buffer-syntactic-context.
-    ;;(?\{ "(}1")
-    ;;(?\} "){4")
-    ;;(?\* ". 23"))
-    ((not (featurep 'xemacs))
-     '(?\{ "(}1b"
-       ?\} "){4b"
-       ?\* ". 23n"))))
+  '(?\$ "."
+    ?\/ "."
+    ?\\ "\\"
+    ?+  "."
+    ?-  "."
+    ?=  "."
+    ?%  "."
+    ?<  "w"
+    ?>  "w"
+    ?\& "."
+    ?.  "w"
+    ?_  "w"
+    ?\' "w"
+    ??  "w"
+    ?`  "\""
+    ?\( "()1"
+    ?\) ")(4"
+    ?\{ "(}1b"
+    ?\} "){4b"
+    ?\* ". 23n")
    "Syntax table entries for Isar scripts.
 This list is in the right format for proof-easy-config.")
 
@@ -363,11 +346,6 @@ matches contents of quotes for quoted identifiers.")
 (defconst isabelle-var-name-face   'isabelle-var-name-face)
 
 
-(defconst isar-font-lock-local
-  '("\\(\\\\<\\^loc>\\)\\([^\\]\\|\\\\<[A-Za-z]+>\\)"
-    (1 x-symbol-invisible-face t)
-    (2 proof-declaration-name-face prepend)))
-
 (defvar isar-font-lock-keywords-1
   (list
    (cons 'isar-match-nesting                               'font-lock-preprocessor-face)
@@ -379,35 +357,35 @@ matches contents of quotes for quoted identifiers.")
    (cons (isar-ids-to-regexp isar-keywords-proof-context)  'proof-declaration-name-face)
    (cons (isar-ids-to-regexp isar-keywords-improper)       'font-lock-reference-face)
    (cons isar-improper-regexp 'font-lock-reference-face)
-   (cons isar-antiq-regexp '(0 'font-lock-variable-name-face t))
-   isar-font-lock-local))
+   (cons isar-antiq-regexp '(0 'font-lock-variable-name-face t))))
+
+;; Indicate we're going to use font lock to manage 'invisible property
+(put 'isar-goals-mode 'font-lock-extra-managed-props '(invisible))
+(put 'isar-response-mode 'font-lock-extra-managed-props '(invisible))
+
+(defun isar-output-flk (start regexp end face)
+  `(,(concat "\\(" start "\\)\\(" regexp "\\)\\(" end "\\)")
+    (1 '(face nil invisible t) prepend)
+    (2 '(face ,face) prepend)
+    (,(+ 3 (regexp-opt-depth regexp)) '(face nil invisible t) prepend)))
 
 (defvar isar-output-font-lock-keywords-1
   (list
-   (cons "\327[^\330]*\330" 'proof-warning-face)
-   (cons (concat "\351" isar-long-id-stuff "\350") 'isabelle-class-name-face)
-   (cons (concat "\352'" isar-id "\350") 'isabelle-tfree-name-face)
-   (cons (concat "\353'" isar-idx "\350") 'isabelle-tvar-name-face)
-   (cons (concat "\353\\?'" isar-idx "\350") 'isabelle-tvar-name-face)
-   (cons (concat "\354" isar-id "\350") 'isabelle-free-name-face)
-   (cons (concat "\355" isar-id "\350") 'isabelle-bound-name-face)
-   (cons (concat "\356" isar-idx "\350") 'isabelle-var-name-face)
-   (cons (concat "\356\\?" isar-idx "\350") 'isabelle-var-name-face)
-   (cons (concat "\357" isar-id "\350") 'proof-declaration-name-face)
-   (cons (concat "\357\\?" isar-idx "\350") 'proof-declaration-name-face)
-   (cons "\^A0\\([^\^A]\\|\^A[^1]\\)*\^A1" 'proof-warning-face)
-   (cons (concat "\^AB" isar-long-id-stuff "\^AA") 'isabelle-class-name-face)
-   (cons (concat "\^AC'" isar-id "\^AA") 'isabelle-tfree-name-face)
-   (cons (concat "\^AD'" isar-idx "\^AA") 'isabelle-tvar-name-face)
-   (cons (concat "\^AD\\?'" isar-idx "\^AA") 'isabelle-tvar-name-face)
-   (cons (concat "\^AE" isar-id "\^AA") 'isabelle-free-name-face)
-   (cons (concat "\^AF" isar-id "\^AA") 'isabelle-bound-name-face)
-   (cons (concat "\^AG" isar-idx "\^AA") 'isabelle-var-name-face)
-   (cons (concat "\^AG\\?" isar-idx "\^AA") 'isabelle-var-name-face)
-   (cons (concat "\^AH" isar-id "\^AA") 'proof-declaration-name-face)
-   (cons (concat "\^AH\\?" isar-idx "\^AA") 'proof-declaration-name-face)
-   isar-font-lock-local)
-  "*Font-lock table for Isabelle terms.")
+   '("\^AI\\|\^AJ\\|\^AK\\|\^AM\\|\^AN\\|\^AO\\|\^AP" (0 '(face nil invisible t) t))
+   (isar-output-flk "\^A0" "\\(?:[^\^A]\\|\^A[^1]\\)*" "\^A1" 'proof-warning-face)
+;; done generically at the moment:
+;;  (isar-output-flk "\^AM" "\\(?:[^\^A]\\|\^A[^N]\\)*" "\^AN" 'proof-error-face)
+   (isar-output-flk "\^AB" isar-long-id-stuff "\^AA" 'isabelle-class-name-face)
+   (isar-output-flk "\^AC'" isar-id "\^AA" 'isabelle-tfree-name-face)
+   (isar-output-flk "\^AD'" isar-idx "\^AA" 'isabelle-tvar-name-face)
+   (isar-output-flk "\^AD\\?'" isar-idx "\^AA" 'isabelle-tvar-name-face)
+   (isar-output-flk "\^AE" isar-id "\^AA" 'isabelle-free-name-face)
+   (isar-output-flk "\^AF" isar-id "\^AA" 'isabelle-bound-name-face)
+   (isar-output-flk "\^AG" isar-idx "\^AA" 'isabelle-var-name-face)
+   (isar-output-flk "\^AG\\?" isar-idx "\^AA" 'isabelle-var-name-face)
+   (isar-output-flk "\^AH" isar-id "\^AA" 'proof-declaration-name-face)
+   (isar-output-flk "\^AH\\?" isar-idx "\^AA" 'proof-declaration-name-face))
+  "*Font-lock table for Isabelle output terms.")
 
 (defvar isar-goals-font-lock-keywords
   (append
diff --git a/isar/isar-unicode-tokens.el b/isar/isar-unicode-tokens.el
index 874b33cb..18e75727 100644
--- a/isar/isar-unicode-tokens.el
+++ b/isar/isar-unicode-tokens.el
@@ -4,479 +4,454 @@
 ;; Copyright(C) 2008 David Aspinall / LFCS Edinburgh
 ;; Author:    David Aspinall <David.Aspinall@ed.ac.uk>
 ;;
-;; This file is loaded by `proof-unicode-tokens.el'.
+;; This file is loaded by proof-auxmodes.el for proof-unicode-tokens.el.
 ;;
 ;; It sets the variables defined at the top of unicode-tokens.el,
 ;; unicode-tokens-<foo> is set from isar-<foo>.  See the corresponding
 ;; variable for documentation.
 ;;
 
-(defconst isar-token-format "\\<%s>")
-(defconst isar-charref-format "\\<#x%x>")
-(defconst isar-token-prefix "\\<")
-(defconst isar-token-suffix ">")
-(defconst isar-token-match "\\\\<\\([a-zA-Z][a-zA-Z0-9_']+\\)>")
-(defconst isar-control-token-match "\\\\<^\\([a-zA-Z][a-zA-Z0-9_']+\\)>")
-(defconst isar-control-token-format "\\<^%s>")
-(defconst isar-hexcode-match "\\\\<\\(#[xX][0-9A-Fa-f]+\\)")
-(defconst isar-next-character-regexp "\\\\<#[xX][0-9A-Fa-f]+>\\|.")
-
-(defcustom isar-token-name-alist
-  (flet 
-      ((script (s) (format "\\<^bscript>%s\\<^escript>" s))
-       (frakt (s) (format "\\<^bfrak>%s\\<^efrak>" s))
-       (serif (s) (format "\\<^bserif>%s\\<^eserif>" s))
-       (bold (s) (format "\\<^bbold>%s\\<^ebold>" s)))
-
-    ;; property-based annotations.  More direct for input
-    ;; but inverse mapping tricky: need to ignore for 
-    ;; reverse and fold \<^bscript>A\<^escript> -> \<AA> etc.
-    ;; Extra dimension in table required.
-    ;; (Also: not supported in XEmacs?)
-      ;((script (s) (unicode-tokens-annotate-string "script" s))
-      ; (frakt    (s) (unicode-tokens-annotate-string "frak" s))
-      ; (serif     (s) (unicode-tokens-annotate-string "serif" s)))
-  `(; token name, unicode char sequence
-    ;; Based on isabellesym.sty,v 1.45 2006/01/05
-
-    ;; Bold numerals
+(require 'proof-unicode-tokens)
+
+;;
+;; Controls
+;;
+
+(defconst isar-control-region-format-regexp
+  "\\(\\\\<\\^%s>\\)\\(.*?\\)\\(\\\\<\\^%s>\\)")
+
+(defconst isar-control-char-format-regexp 
+  "\\(\\\\<\\^%s>\\)\\([^\\]\\|\\\\<[A-Za-z]+>\\)")
+
+(defconst isar-control-region-format-beg "\\<^%s>")
+(defconst isar-control-region-format-end "\\<^%s>")
+(defconst isar-control-char-format "\\<^%s>")
+
+
+(defconst isar-control-characters
+  '(("Subscript" "sub" sub) 
+    ("Id subscript" "isub" sub)
+    ("Superscript" "sup" sup) 
+    ("Id superscript" "isup" sup)
+    ("Loc" "loc" loc)
+    ("Bold" "bold" bold) 
+    ("Italic" "italic" italic))) ; unofficial
+
+(defconst isar-control-regions
+  '(("Subscript" "bsub" "esub" sub)
+    ("Superscript" "bsup" "esup" sup) 
+    ; unofficial:
+    ("Bold" "bbold" "ebold" bold)
+    ("Italic" "bitalic" "eitalic" italic)
+    ("Script" "bscript" "escript" script)
+    ("Frakt" "bfrakt" "efrakt" frakt)
+    ("Roman" "bserif" "eserif" serif)))
+    
+(defcustom isar-fontsymb-properties 
+  '((sub      (display (raise -0.4)))
+    (sup      (display (raise 0.4)))
+    (loc      (face proof-declaration-name-face))
+    (bold     (face (:weight bold)))
+    (italic   (face (:slant italic)))
+    (script   (face unicode-tokens-script-font-face))
+    (frakt    (face unicode-tokens-fraktur-font-face))
+    (serif    (face unicode-tokens-serif-font-face)))
+  "Mapping from symbols to property lists used for markup scheme."
+  :set 'proof-set-value)
+
 ;;
-;; These are unreliable so removed for release version.
-;; 
-;;;     ("zero" . ,(bold "0"))
-;;;     ("one" . ,(bold "1"))
-;;;     ("two" . ,(bold "2"))
-;;;     ("three" . ,(bold "3"))
-;;;     ("four" . ,(bold "4"))
-;;;     ("five" . ,(bold "5"))
-;;;     ("six" . ,(bold "6"))
-;;;     ("seven" . ,(bold "7"))
-;;;     ("eight" . ,(bold "8"))
-;;;     ("nine" . ,(bold "9"))
-;;;     ;; Mathcal 
-;;;     ("A" . ,(script "A"))
-;;;     ("B" . ,(script "B"))
-;;;     ("C" . ,(script "C"))
-;;;     ("D" . ,(script "D"))
-;;;     ("E" . ,(script "E"))
-;;;     ("F" . ,(script "F"))
-;;;     ("G" . ,(script "G"))
-;;;     ("H" . ,(script "H"))
-;;;     ("I" . ,(script "I"))
-;;;     ("J" . ,(script "J"))
-;;;     ("K" . ,(script "K"))
-;;;     ("L" . ,(script "L"))
-;;;     ("M" . ,(script "M"))
-;;;     ("N" . ,(script "N"))
-;;;     ("O" . ,(script "O"))
-;;;     ("P" . ,(script "P"))
-;;;     ("Q" . ,(script "Q"))
-;;;     ("R" . ,(script "R"))
-;;;     ("S" . ,(script "S"))
-;;;     ("T" . ,(script "T"))
-;;;     ("U" . ,(script "U"))
-;;;     ("V" . ,(script "V"))
-;;;     ("W" . ,(script "W"))
-;;;     ("X" . ,(script "X"))
-;;;     ("Y" . ,(script "Y"))
-;;;     ("Z" . ,(script "Z"))
-;;;     ;; Math roman
-;;;     ("a" . ,(serif "a"))
-;;;     ("b" . ,(serif "b"))
-;;;     ("c" . ,(serif "c"))
-;;;     ("d" . ,(serif "d"))
-;;;     ("e" . ,(serif "e"))
-;;;     ("f" . ,(serif "f"))
-;;;     ("g" . ,(serif "g"))
-;;;     ("h" . ,(serif "h"))
-;;;     ("i" . ,(serif "i"))
-;;;     ("j" . ,(serif "j"))
-;;;     ("k" . ,(serif "k"))
-;;;     ("l" . ,(serif "l"))
-;;;     ("m" . ,(serif "m"))
-;;;     ("n" . ,(serif "n"))
-;;;     ("o" . ,(serif "o"))
-;;;     ("p" . ,(serif "p"))
-;;;     ("q" . ,(serif "q"))
-;;;     ("r" . ,(serif "r"))
-;;;     ("s" . ,(serif "s"))
-;;;     ("t" . ,(serif "t"))
-;;;     ("u" . ,(serif "u"))
-;;;     ("v" . ,(serif "v"))
-;;;     ("w" . ,(serif "w"))
-;;;     ("x" . ,(serif "x"))
-;;;     ("y" . ,(serif "y"))
-;;;     ("z" . ,(serif "z"))
-;;;     ;; Fraktur
-;;;     ("AA" . ,(frakt "A"))
-;;;     ("BB" . ,(frakt "B"))
-;;;     ("CC" . ,(frakt "C"))
-;;;     ("DD" . ,(frakt "D"))
-;;;     ("EE" . ,(frakt "E"))
-;;;     ("FF" . ,(frakt "F"))
-;;;     ("GG" . ,(frakt "G"))
-;;;     ("HH" . ,(frakt "H"))
-;;;     ("II" . ,(frakt "I"))
-;;;     ("JJ" . ,(frakt "J"))
-;;;     ("KK" . ,(frakt "K"))
-;;;     ("LL" . ,(frakt "L"))
-;;;     ("MM" . ,(frakt "M"))
-;;;     ("NN" . ,(frakt "N"))
-;;;     ("OO" . ,(frakt "O"))
-;;;     ("PP" . ,(frakt "P"))
-;;;     ("QQ" . ,(frakt "Q"))
-;;;     ("RR" . ,(frakt "R"))
-;;;     ("SS" . ,(frakt "S"))
-;;;     ("TT" . ,(frakt "T"))
-;;;     ("UU" . ,(frakt "U"))
-;;;     ("VV" . ,(frakt "V"))
-;;;     ("WW" . ,(frakt "W"))
-;;;     ("XX" . ,(frakt "X"))
-;;;     ("YY" . ,(frakt "Y"))
-;;;     ("ZZ" . ,(frakt "Z"))
-;;;     ("aa" . ,(frakt "a"))
-;;;     ("bb" . ,(frakt "b"))
-;;;     ("cc" . ,(frakt "c"))
-;;;     ("dd" . ,(frakt "d"))
-;;;     ("ee" . ,(frakt "e"))
-;;;     ("ff" . ,(frakt "f"))
-;;;     ("gg" . ,(frakt "g"))
-;;;     ("hh" . ,(frakt "h"))
-;;;     ("ii" . ,(frakt "i"))
-;;;     ("jj" . ,(frakt "j"))
-;;;     ("kk" . ,(frakt "k"))
-;;;     ("ll" . ,(frakt "l"))
-;;;     ("mm" . ,(frakt "m"))
-;;;     ("nn" . ,(frakt "n"))
-;;;     ("oo" . ,(frakt "o"))
-;;;     ("pp" . ,(frakt "p"))
-;;;     ("qq" . ,(frakt "q"))
-;;;     ("rr" . ,(frakt "r"))
-;;;     ("ss" . ,(frakt "s"))
-;;;     ("tt" . ,(frakt "t"))
-;;;     ("uu" . ,(frakt "u"))
-;;;     ("vv" . ,(frakt "v"))
-;;;     ("ww" . ,(frakt "w"))
-;;;     ("xx" . ,(frakt "x"))
-;;;     ("yy" . ,(frakt "y"))
-;;;     ("zz" . ,(frakt "z"))
-    ("alpha" . "α")
-    ("beta" . "β")
-    ("gamma" . "γ")
-    ("delta" . "δ")
-    ("epsilon" . "ε") ; actually varepsilon (some is epsilon)
-    ("zeta" . "ζ")
-    ("eta" . "η")
-    ("theta" . "θ")
-    ("iota" . "ι")
-    ("kappa" . "κ")
-    ("lambda" . "λ")
-    ("mu" . "μ")
-    ("nu" . "ν")
-    ("xi" . "ξ")
-    ("pi" . "π")
-    ("rho" . "ρ")
-    ("sigma" . "σ")
-    ("tau" . "τ")
-    ("upsilon" . "υ")
-    ("phi" . "ϕ")
-    ("chi" . "χ")
-    ("psi" . "ψ")
-    ("omega" . "ω")
-    ("Gamma" . "Γ")
-    ("Delta" . "Δ")
-    ("Theta" . "Θ")
-    ("Lambda" . "Λ")
-    ("Xi" . "Ξ")
-    ("Pi" . "Π")
-    ("Sigma" . "Σ")
-    ("Upsilon" . "Υ")
-    ("Phi" . "Φ")
-    ("Psi" . "Ψ")
-    ("Omega" . "Ω")
-;;  ("bool" . "")
-    ("complex" . "ℂ")
-    ("nat" . "ℕ")
-    ("rat" . "ℚ")
-    ("real" . "ℝ")
-    ("int" . "ℤ")
-    ;; Arrows
-    ("leftarrow" . "←")
-    ("rightarrow" . "→")
-    ("Leftarrow" . "⇐")
-    ("Rightarrow" . "⇒")
-    ("leftrightarrow" . "↔")
-    ("Leftrightarrow" . "⇔")
-    ("mapsto" . "↦")
-    ;; Real long symbols, may work in some places
-    ("longleftarrow" . "⟵")
-    ("Longleftarrow" . "⟸")
-    ("longrightarrow" . "⟶")
-    ("Longrightarrow" . "⟹")
-    ("longleftrightarrow" . "⟷")
-    ("Longleftrightarrow" . "⟺")
-    ("longmapsto" . "⟼")
-    ;; Faked long symbols, for use otherwise:
-;;;     ("longleftarrow" . "←–")
-;;;     ("Longleftarrow" . "⇐–")
-;;;     ("longrightarrow" . "–→")
-;;;     ("Longrightarrow" . "–⇒")
-;;;     ("longleftrightarrow" . "←→")
-;;;     ("Longleftrightarrow" . "⇐⇒")
-;;;     ("longmapsto" . "❘→")
-    ("midarrow" . "–") ; #x002013 en dash
-    ("Midarrow" . "‗") ; #x002017 double low line (not mid)
-    ("hookleftarrow" . "↩")
-    ("hookrightarrow" . "↪")
-    ("leftharpoondown" . "↽")
-    ("rightharpoondown" . "⇁")
-    ("leftharpoonup" . "↼")
-    ("rightharpoonup" . "⇀")
-    ("rightleftharpoons" . "⇌")
-    ("leadsto" . "↝")
-    ("downharpoonleft" . "⇃")
-    ("downharpoonright" . "⇂")
-    ("upharpoonleft" . "↿")
-    ;; ("upharpoonright" . "↾") overlaps restriction
-    ("restriction" . "↾") ;; 
-    ("Colon" . "∷")
-    ("up" . "↑")
-    ("Up" . "⇑")
-    ("down" . "↓")
-    ("Down" . "⇓")
-    ("updown" . "↕")
-    ("Updown" . "⇕")
-    ("langle" . "⟪")
-    ("rangle" . "⟫")
-    ("lceil" . "⌈")
-    ("rceil" . "⌉")
-    ("lfloor" . "⌊")
-    ("rfloor" . "⌋")
-    ("lparr" . "⦇")
-    ("rparr" . "⦈")
-    ("lbrakk" . "⟦")
-    ("rbrakk" . "⟧")
-    ("lbrace" . "⦃")
-    ("rbrace" . "⦄")
-    ("guillemotleft" . "«")
-    ("guillemotright" . "»")
-    ("bottom" . "⊥")
-    ("top" . "⊤")
-    ("and" . "∧")
-    ("And" . "⋀")
-    ("or" . "∨")
-    ("Or" . "⋁")
-    ("forall" . "∀")
-    ("exists" . "∃")
-    ("nexists" . "∄")
-    ("not" . "¬")
-    ("box" . "□")
-    ("diamond" . "◇")
-    ("turnstile" . "⊢")
-    ("Turnstile" . "⊨")
-    ("tturnstile" . "⊩")
-    ("TTurnstile" . "⊫")
-    ("stileturn" . "⊣")
-    ("surd" . "√")
-    ("le" . "≤")
-    ("ge" . "≥")
-    ("lless" . "≪")
-    ("ggreater" . "≫")
-    ("lesssim" . "⪍")
-    ("greatersim" . "⪎")
-    ("lessapprox" . "⪅")
-    ("greaterapprox" . "⪆")
-    ("in" . "∈")
-    ("notin" . "∉")
-    ("subset" . "⊂")
-    ("supset" . "⊃")
-    ("subseteq" . "⊆")
-    ("supseteq" . "⊇")    
-    ("sqsubset" . "⊏")
-    ("sqsupset" . "⊐")
-    ("sqsubseteq" . "⊑")
-    ("sqsupseteq" . "⊒")
-    ("inter" . "∩")
-    ("Inter" . "⋂")
-    ("union" . "∪")
-    ("Union" . "⋃")
-    ("squnion" . "⊔")
-    ("Squnion" . "⨆")
-    ("sqinter" . "⊓")
-    ("Sqinter" . "⨅")
-    ("setminus" . "∖")
-    ("propto" . "∝")
-    ("uplus" . "⊎")
-    ("Uplus" . "⨄")
-    ("noteq" . "≠")
-    ("sim" . "∼")
-    ("doteq" . "≐")
-    ("simeq" . "≃")
-    ("approx" . "≈")
-    ("asymp" . "≍")
-    ("cong" . "≅")
-    ("smile" . "⌣")
-    ("equiv" . "≡")
-    ("frown" . "⌢")
-    ("Join" . "⨝")
-    ("bowtie" . "⋈")
-    ("prec" . "≺")
-    ("succ" . "≻")
-    ("preceq" . "≼")
-    ("succeq" . "≽")
-    ("parallel" . "∥")
-    ("bar" . "¦")
-    ("plusminus" . "±")
-    ("minusplus" . "∓")
-    ("times" . "×")
-    ("div" . "÷")
-    ("cdot" . "⋅")
-    ("star" . "⋆")
-    ("bullet" . "∙")
-    ("circ" . "∘")
-    ("dagger" . "†")
-    ("ddagger" . "‡")
-    ("lhd" . "⊲")
-    ("rhd" . "⊳")
-    ("unlhd" . "⊴")
-    ("unrhd" . "⊵")
-    ("triangleleft" . "◁")
-    ("triangleright" . "▷")
-    ("triangle" . "▵") ; or △
-    ("triangleq" . "≜")
-    ("oplus" . "⊕")
-    ("Oplus" . "⨁")
-    ("otimes" . "⊗")
-    ("Otimes" . "⨂")
-    ("odot" . "⊙")
-    ("Odot" . "⨀")
-    ("ominus" . "⊖")
-    ("oslash" . "⊘") 
-    ("dots" . "…")
-    ("cdots" . "⋯")
-    ("Sum" . "∑")
-    ("Prod" . "∏")
-    ("Coprod" . "∐")
-    ("infinity" . "∞")
-    ("integral" . "∫")
-    ("ointegral" . "∮")
-    ("clubsuit" . "♣")
-    ("diamondsuit" . "♢")
-    ("heartsuit" . "♡")
-    ("spadesuit" . "♠")
-    ("aleph" . "ℵ")
-    ("emptyset" . "∅")
-    ("nabla" . "∇")
-    ("partial" . "∂")
-    ("Re" . "ℜ")
-    ("Im" . "ℑ")
-    ("flat" . "♭")
-    ("natural" . "♮")
-    ("sharp" . "♯")
-    ("angle" . "∠")
-    ("copyright" . "©")
-    ("registered" . "®")
-    ("hyphen" . "‐")
-    ("inverse" . "¯¹") ; X-Symb: just "¯"
-    ("onesuperior" . "¹")
-    ("twosuperior" . "²")
-    ("threesuperior" . "³")
-    ("onequarter" . "¼")
-    ("onehalf" . "½")
-    ("threequarters" . "¾")
-    ("ordmasculine" . "º")
-    ("ordfeminine" . "ª")
-    ("section" . "§")
-    ("paragraph" . "¶")
-    ("exclamdown" . "¡")
-    ("questiondown" . "¿")
-    ("euro" . "€")
-    ("pounds" . "£")
-    ("yen" . "¥")
-    ("cent" . "¢")
-    ("currency" . "¤")
-    ("degree" . "°")
-    ("amalg" . "⨿")
-    ("mho" . "℧")
-    ("lozenge" . "◊")
-    ("wp" . "℘")
-    ("wrong" . "≀") ;; #x002307
-;;    ("struct" . "") ;; TODO
-    ("acute" . "´")
-    ("index" . "ı")
-    ("dieresis" . "¨")
-    ("cedilla" . "¸")
-    ("hungarumlaut" . "ʺ")
-    ("spacespace" . "⁣⁣") ;; two #x002063
-;    ("module" . "") ??
-    ("some" . "ϵ")
+;; Symbols
+;;
+
+(defconst isar-token-format "\\<%s>")
+
+;(defconst isar-token-variant-format-regexp 
+;  "\\\\<\\(%s\\)\\([:][a-zA-Z0-9]+\\)?>") ; syntax change required
+(defconst isar-token-variant-format-regexp 
+  "\\\\<\\(%s\\)\\([0-9]+\\)?>") ; unofficial interpretation of usual syntax
+
+(defconst isar-greek-letters-tokens
+  '(("alpha" "α")
+    ("beta" "β")
+    ("gamma" "γ")
+    ("delta" "δ")
+    ("epsilon" "ε") ; actually varepsilon (some is epsilon)
+    ("zeta" "ζ")
+    ("eta" "η")
+    ("theta" "θ")
+    ("iota" "ι")
+    ("kappa" "κ")
+    ("lambda" "λ")
+    ("mu" "μ")
+    ("nu" "ν")
+    ("xi" "ξ")
+    ("pi" "π")
+    ("rho" "ρ")
+    ("sigma" "σ")
+    ("tau" "τ")
+    ("upsilon" "υ")
+    ("phi" "ϕ")
+    ("chi" "χ")
+    ("psi" "ψ")
+    ("omega" "ω")
+    ("Gamma" "Γ")
+    ("Delta" "Δ")
+    ("Theta" "Θ")
+    ("Lambda" "Λ")
+    ("Xi" "Ξ")
+    ("Pi" "Π")
+    ("Sigma" "Σ")
+    ("Upsilon" "Υ")
+    ("Phi" "Φ")
+    ("Psi" "Ψ")
+    ("Omega" "Ω")))
+
+(defconst isar-misc-letters-tokens
+  '(("bool" "IB")
+    ("complex" "ℂ")
+    ("nat" "ℕ")
+    ("rat" "ℚ")
+    ("real" "ℝ")
+    ("int" "ℤ")))
+
+(defconst isar-symbols-tokens
+  '(("leftarrow" "←")
+    ("rightarrow" "→")
+    ("Leftarrow" "⇐")
+    ("Rightarrow" "⇒")
+    ("leftrightarrow" "↔")
+    ("Leftrightarrow" "⇔")
+    ("mapsto" "↦")
+    ("longleftarrow" "⟵")
+    ("Longleftarrow" "⟸")
+    ("longrightarrow" "⟶")
+    ("Longrightarrow" "⟹")
+    ("longleftrightarrow" "⟷")
+    ("Longleftrightarrow" "⟺")
+    ("longmapsto" "⟼")
+    ("midarrow" "–") ; #x002013 en dash
+    ("Midarrow" "‗") ; #x002017 double low line (not mid)
+    ("hookleftarrow" "↩")
+    ("hookrightarrow" "↪")
+    ("leftharpoondown" "↽")
+    ("rightharpoondown" "⇁")
+    ("leftharpoonup" "↼")
+    ("rightharpoonup" "⇀")
+    ("rightleftharpoons" "⇌")
+    ("leadsto" "↝")
+    ("downharpoonleft" "⇃")
+    ("downharpoonright" "⇂")
+    ("upharpoonleft" "↿")  ;; 
+    ("upharpoonright" "↾") ;; overlaps restriction
+    ("restriction" "↾")    ;; same as above
+    ("Colon" "∷")
+    ("up" "↑")
+    ("Up" "⇑")
+    ("down" "↓")
+    ("Down" "⇓")
+    ("updown" "↕")
+    ("Updown" "⇕")
+    ("langle" "⟨")
+    ("rangle" "⟩")
+    ("lceil" "⌈")
+    ("rceil" "⌉")
+    ("lfloor" "⌊")
+    ("rfloor" "⌋")
+    ("lparr" "⦇")
+    ("rparr" "⦈")
+    ("lbrakk" "⟦")
+    ("rbrakk" "⟧")
+    ("lbrace" "⦃")
+    ("rbrace" "⦄")
+    ("guillemotleft" "«")
+    ("guillemotright" "»")
+    ("bottom" "⊥")
+    ("top" "⊤")
+    ("and" "∧")
+    ("And" "⋀")
+    ("or" "∨")
+    ("Or" "⋁")
+    ("forall" "∀")
+    ("exists" "∃")
+    ("nexists" "∄")
+    ("not" "¬")
+    ("box" "□")
+    ("diamond" "◇")
+    ("turnstile" "⊢")
+    ("Turnstile" "⊨")
+    ("tturnstile" "⊩")
+    ("TTurnstile" "⊫")
+    ("stileturn" "⊣")
+    ("surd" "√")
+    ("le" "≤")
+    ("ge" "≥")
+    ("lless" "≪")
+    ("ggreater" "≫")
+    ("lesssim" "⪍")
+    ("greatersim" "⪎")
+    ("lessapprox" "⪅")
+    ("greaterapprox" "⪆")
+    ("in" "∈")
+    ("notin" "∉")
+    ("subset" "⊂")
+    ("supset" "⊃")
+    ("subseteq" "⊆")
+    ("supseteq" "⊇")    
+    ("sqsubset" "⊏")
+    ("sqsupset" "⊐")
+    ("sqsubseteq" "⊑")
+    ("sqsupseteq" "⊒")
+    ("inter" "∩")
+    ("Inter" "⋂")
+    ("union" "∪")
+    ("Union" "⋃")
+    ("squnion" "⊔")
+    ("Squnion" "⨆")
+    ("sqinter" "⊓")
+    ("Sqinter" "⨅")
+    ("setminus" "∖")
+    ("propto" "∝")
+    ("uplus" "⊎")
+    ("Uplus" "⨄")
+    ("noteq" "≠")
+    ("sim" "∼")
+    ("doteq" "≐")
+    ("simeq" "≃")
+    ("approx" "≈")
+    ("asymp" "≍")
+    ("cong" "≅")
+    ("smile" "⌣")
+    ("equiv" "≡")
+    ("frown" "⌢")
+    ("Join" "⨝")
+    ("bowtie" "⋈")
+    ("prec" "≺")
+    ("succ" "≻")
+    ("preceq" "≼")
+    ("succeq" "≽")
+    ("parallel" "∥")
+    ("bar" "¦")
+    ("plusminus" "±")
+    ("minusplus" "∓")
+    ("times" "×")
+    ("div" "÷")
+    ("cdot" "⋅")
+    ("star" "⋆")
+    ("bullet" "∙")
+    ("circ" "∘")
+    ("dagger" "†")
+    ("ddagger" "‡")
+    ("lhd" "⊲")
+    ("rhd" "⊳")
+    ("unlhd" "⊴")
+    ("unrhd" "⊵")
+    ("triangleleft" "◁")
+    ("triangleright" "▷")
+    ("triangle" "▵") ; or △
+    ("triangleq" "≜")
+    ("oplus" "⊕")
+    ("Oplus" "⨁")
+    ("otimes" "⊗")
+    ("Otimes" "⨂")
+    ("odot" "⊙")
+    ("Odot" "⨀")
+    ("ominus" "⊖")
+    ("oslash" "⊘") 
+    ("dots" "…")
+    ("cdots" "⋯")
+    ("Sum" "∑")
+    ("Prod" "∏")
+    ("Coprod" "∐")
+    ("infinity" "∞")
+    ("integral" "∫")
+    ("ointegral" "∮")
+    ("clubsuit" "♣")
+    ("diamondsuit" "♢")
+    ("heartsuit" "♡")
+    ("spadesuit" "♠")
+    ("aleph" "ℵ")
+    ("emptyset" "∅")
+    ("nabla" "∇")
+    ("partial" "∂")
+    ("Re" "ℜ")
+    ("Im" "ℑ")
+    ("flat" "♭")
+    ("natural" "♮")
+    ("sharp" "♯")
+    ("angle" "∠")
+    ("copyright" "©")
+    ("registered" "®")
+    ("hyphen" "‐")
+    ("inverse" "¯¹") ; X-Symb: just "¯"
+    ("onesuperior" "¹")
+    ("twosuperior" "²")
+    ("threesuperior" "³")
+    ("onequarter" "¼")
+    ("onehalf" "½")
+    ("threequarters" "¾")
+    ("ordmasculine" "º")
+    ("ordfeminine" "ª")
+    ("section" "§")
+    ("paragraph" "¶")
+    ("exclamdown" "¡")
+    ("questiondown" "¿")
+    ("euro" "€")
+    ("pounds" "£")
+    ("yen" "¥")
+    ("cent" "¢")
+    ("currency" "¤")
+    ("degree" "°")
+    ("amalg" "⨿")
+    ("mho" "℧")
+    ("lozenge" "◊")
+    ("wp" "℘")
+    ("wrong" "≀") ;; #x002307
+;;    ("struct" "") ;; TODO
+    ("acute" "´")
+    ("index" "ı")
+    ("dieresis" "¨")
+    ("cedilla" "¸")
+    ("hungarumlaut" "ʺ")
+    ("spacespace" "⁣⁣") ;; two #x002063
+;    ("module" "") ??
+    ("some" "ϵ")
     
     ;; Not in Standard Isabelle Symbols
     ;; (some are in X-Symbols)
 
-    ("stareq" . "≛")
-    ("defeq" . "≝")
-    ("questioneq" . "≟")
-    ("vartheta" . "ϑ")
-    ; ("o" . "ø")
-    ("varpi" . "ϖ")
-    ("varrho" . "ϱ")
-    ("varsigma" . "ς")
-    ("varphi" . "φ")
-    ("hbar" . "ℏ")
-    ("ell" . "ℓ")
-    ("ast" . "∗")
-
-    ("bigcirc" . "◯")
-    ("bigtriangleup" . "△")
-    ("bigtriangledown" . "▽")
-    ("ni" . "∋")
-    ("mid" . "∣")
-    ("notlt" . "≮")
-    ("notle" . "≰")
-    ("notprec" . "⊀")
-    ("notpreceq" . "⋠")
-    ("notsubset" . "⊄")
-    ("notsubseteq" . "⊈")
-    ("notsqsubseteq" . "⋢")
-    ("notgt" . "≯")
-    ("notge" . "≱")
-    ("notsucc" . "⊁")
-    ("notsucceq" . "⋡")
-    ("notsupset" . "⊅")
-    ("notsupseteq" . "⊉")
-    ("notsqsupseteq" . "⋣")
-    ("notequiv" . "≢")
-    ("notsim" . "≁")
-    ("notsimeq" . "≄")
-    ("notapprox" . "≉")
-    ("notcong" . "≇")
-    ("notasymp" . "≭")
-    ("nearrow" . "↗")
-    ("searrow" . "↘")
-    ("swarrow" . "↙")
-    ("nwarrow" . "↖")
-    ("vdots" . "⋮")
-    ("ddots" . "⋱")
-    ("closequote" . "’")
-    ("openquote" . "‘")
-    ("opendblquote" . "”")
-    ("closedblquote" . "“")
-    ("emdash" . "—")
-    ("prime" . "′")
-    ("doubleprime" . "″")
-    ("tripleprime" . "‴")
-    ("quadrupleprime" . "⁗")
-    ("nbspace" . " ")
-    ("thinspace" . " ")
-    ("notni" . "∌")
-    ("colonequals" . "≔")
-    ("foursuperior" . "⁴")
-    ("fivesuperior" . "⁵")
-    ("sixsuperior" . "⁶")
-    ("sevensuperior" . "⁷")
-    ("eightsuperior" . "⁸")
-    ("ninesuperior" . "⁹")))
+    ("stareq" "≛")
+    ("defeq" "≝")
+    ("questioneq" "≟")
+    ("vartheta" "ϑ")
+    ; ("o" "ø")
+    ("varpi" "ϖ")
+    ("varrho" "ϱ")
+    ("varsigma" "ς")
+    ("varphi" "φ")
+    ("hbar" "ℏ")
+    ("ell" "ℓ")
+    ("ast" "∗")
+
+    ("bigcirc" "◯")
+    ("bigtriangleup" "△")
+    ("bigtriangledown" "▽")
+    ("ni" "∋")
+    ("mid" "∣")
+    ("notlt" "≮")
+    ("notle" "≰")
+    ("notprec" "⊀")
+    ("notpreceq" "⋠")
+    ("notsubset" "⊄")
+    ("notsubseteq" "⊈")
+    ("notsqsubseteq" "⋢")
+    ("notgt" "≯")
+    ("notge" "≱")
+    ("notsucc" "⊁")
+    ("notsucceq" "⋡")
+    ("notsupset" "⊅")
+    ("notsupseteq" "⊉")
+    ("notsqsupseteq" "⋣")
+    ("notequiv" "≢")
+    ("notsim" "≁")
+    ("notsimeq" "≄")
+    ("notapprox" "≉")
+    ("notcong" "≇")
+    ("notasymp" "≭")
+    ("nearrow" "↗")
+    ("searrow" "↘")
+    ("swarrow" "↙")
+    ("nwarrow" "↖")
+    ("vdots" "⋮")
+    ("ddots" "⋱")
+    ("closequote" "’")
+    ("openquote" "‘")
+    ("opendblquote" "”")
+    ("closedblquote" "“")
+    ("emdash" "—")
+    ("prime" "′")
+    ("doubleprime" "″")
+    ("tripleprime" "‴")
+    ("quadrupleprime" "⁗")
+    ("nbspace" " ")
+    ("thinspace" " ")
+    ("notni" "∌")
+    ("colonequals" "≔")
+    ("foursuperior" "⁴")
+    ("fivesuperior" "⁵")
+    ("sixsuperior" "⁶")
+    ("sevensuperior" "⁷")
+    ("eightsuperior" "⁸")
+    ("ninesuperior" "⁹")))
+
+(defun isar-try-char (charset code1 code2)
+  (and (charsetp charset) ; prevent error
+       (char-to-string (make-char charset code1 code2))))
+
+(defconst isar-symbols-tokens-fallbacks
+  `(;; Faked long symbols
+    ("longleftarrow" "←–")
+    ("Longleftarrow" "⇐–")
+    ("longrightarrow" "–→")
+    ("Longrightarrow" "–⇒")
+    ("longleftrightarrow" "←→")
+    ("Longleftrightarrow" "⇐⇒")
+    ("longmapsto" "❘→")
+    ;; bracket composition alternatives
+    ("lparr" "(|")  
+    ("rparr" "|)") 
+    ;; an example of using characters from another charset.
+    ;; to expand this table, see output of M-x list-charset-chars
+    ("lbrakk" ,(isar-try-char 'japanese-jisx0208 #x22 #x5A))
+    ("rbrakk" ,(isar-try-char 'japanese-jisx0208 #x22 #x5B))
+    ("lbrakk" "[|")
+    ("rbrakk" "|]")
+    ("lbrace" "{|")
+    ("rbrace" "|}"))
+  "Fallback alternatives to `isar-symbols-tokens'.
+The first displayable composition will be displayed to replace the
+tokens.")
+
+(defconst isar-bold-nums-tokens 
+  '(("zero" "0" bold)
+    ("one" "1" bold)
+    ("two" "2" bold)
+    ("three" "3" bold)
+    ("four" "4" bold)
+    ("five" "5" bold)
+    ("six" "6" bold)
+    ("seven" "7" bold)
+    ("eight" "8" bold)
+    ("nine" "9" bold)))
+
+(defun isar-map-letters (f1 f2 &rest symbs)
+  (loop for x below 26
+	for c = (+ 65 x)
+	collect 
+	(cons (funcall f1 c) (cons (funcall f2 c) symbs))))
+
+(defconst isar-script-letters-tokens
+  (isar-map-letters (lambda (x) (format "%c" x))
+		    (lambda (x) (format "%c" x))
+		    'script))
+
+(defconst isar-roman-letters-tokens
+  (isar-map-letters (lambda (x) (format "%c" x))
+		    (lambda (x) (format "%c" x))
+		    'serif))
+
+(defconst isar-fraktur-letters-tokens
+  (isar-map-letters (lambda (x) (format "%c%c" x x))
+		    (lambda (x) (format "%c" x))
+		    'frakt))
+  
+(defcustom isar-token-symbol-map
+  (append
+   isar-symbols-tokens
+   isar-symbols-tokens-fallbacks
+   isar-greek-letters-tokens
+   isar-bold-nums-tokens
+   isar-script-letters-tokens
+   isar-roman-letters-tokens)
   "Table mapping Isabelle symbol token names to Unicode strings.
 
 You can adjust this table to add more entries, or to change entries for
@@ -486,94 +461,86 @@ The token TNAME is made into the token \\< TNAME >.
 The string mapping can be anything, but should be such that
 tokens can be uniquely recovered from a decoded text; otherwise
 results will be undefined when files are saved."
-  :type '(repeat (cons (string :tag "Token name")
+  :type '(repeat (list (string :tag "Token name")
 		       (string :tag "Unicode string")))
   :set 'proof-set-value
   :group 'isabelle
   :tag "Isabelle Unicode Token Mapping")
 
 
-(defcustom isar-shortcut-alist
-  '(; short cut, unicode string
-;    ("<>" . "⋄")
-;    ("|>" . "⊳")
-    ("\\/" . "∨")
-    ("/\\" . "∧")
-    ("+O" . "⊕")
-    ("-O" . "⊖")
-    ("xO" . "⊗")
-    ("/O" . "⊘")
-    (".O" . "⊙")
-    ("|+" . "†")
-    ("|++" . "‡")
-    ("<=" . "≤")
-    ("|-" . "⊢")
-    (">=" . "≥")
-    ("-|" . "⊣")
-    ("||" . "∥")
-    ("==" . "≡")
-    ("~=" . "≠")
-    ("~:" . "∉")
+
+(defconst isar-symbol-shortcuts
+;    ("<>" . "\<diamond>")
+;    ("|>" . "\<triangleright>")
+  '(("\\/" . "\\<or>")
+    ("/\\" . "\\<and>")
+    ("+O" . "\\<oplus>")
+    ("-O" . "\\<ominus>")
+    ("xO" . "\\<otimes>")
+    ("/O" . "\\<oslash>")
+    (".O" . "\\<odot>")
+    ("|+" . "\\<dagger>")
+    ("|++" . "\\<ddagger>")
+    ("<=" . "\\<le>")
+    ("|-" . "\\<turnstile>")
+    (">=" . "\\<ge>")
+    ("-|" . "\\<stileturn>")
+    ("||" . "\\<parallel>")
+    ("==" . "\\<equiv>")
+    ("~=" . "\\<noteq>")
+    ("~:" . "\\<notin>")
 ;    ("~=" . "≃")
-    ("~~~" . "≍")
-    ("~~" . "≈")
-    ("~==" . "≅")
-    ("|<>|" . "⋈")
-    ("|=" . "⊨")
-    ("=." . "≐")
-    ("_|_" . "⊥")
-    ("</" . "≮")
-    (">=/" . "≱")
-    ("=/" . "≠")
+    ("~~~" . "\\<notapprox>")
+    ("~~" . "\\<approx>")
+    ("~==" . "\\<cong>")
+    ("|<>|" . "\\<bowtie>")
+    ("|=" . "\\<Turnstile>")
+    ("=." . "\\<doteq>")
+    ("_|_" . "\\<bottom>")
+    ("</" . "\\<notle>")
+    ("~>=" . "\\<notge>")
     ("==/" . "≢")
-    ("~/" . "≁")
-    ("~=/" . "≄")
-    ("~~/" . "≉")
-    ("~==/" . "≇")
-    ("<-" . "←")
-;    ("<=" . "⇐")
-    ("->" . "→")
-    ("=>" . "⇒")
-    ("<->" . "↔")
-    ("<=>" . "⇔")
-    ("|->" . "↦") 
-    ("<--" . "⟵")
-    ("<==" . "⟸")
-    ("-->" . "⟶")
-    ("==>" . "⟹")
-    ("<==>" . "⟷")
-    ("|-->" . "⟼")
-    ("<-->" . "⟷")
-    ("<<" . "«")
-    ("[|" . "⟦")
-    (">>" . "»")
-    ("|]" . "⟧")
-;    ("``" . "”")
-;    ("''" . "“")
-;    ("--" . "–")
-    ("---" . "—")
-;    ("''" . "″")
-;    ("'''" . "‴")
-;    ("''''" . "⁗")
-;    (":=" . "≔")
-    ;; some word shortcuts, started with backslash otherwise
-    ;; too annoying.
-    ("\\nat" . "ℕ")
-    ("\\int" . "ℤ")
-    ("\\rat" . "ℚ")
-    ("\\real" . "ℝ")
-    ("\\complex" . "ℂ")
-    ("\\euro" . "€")
-    ("\\yen" . "¥")
-    ("\\cent" . "¢"))
-  "Shortcut key sequence table for Unicode strings.
+    ("~/" . "\\<notsim>")
+    ("~=/" . "\\<notsimeq>")
+    ("~~/" . "\\<notsimeq>")
+    ("<-" . "\\<leftarrow>")
+;    ("<=" . "\\<Leftarrow>")
+    ("->" . "\\<rightarrow>")
+    ("=>" . "\\<Rightarrow>")
+    ("<->" . "\\<leftrightarrow>")
+    ("<=>" . "\\<Leftrightarrow>")
+    ("|->" . "\\<mapsto>") 
+    ("<--" . "\\<longleftarrow>")
+    ("<==" . "\\<Longleftarrow>")
+    ("-->" . "\\<longrightarrow>")
+    ("==>" . "\\<Longrightarrow>")
+    ("<==>" . "\\<Longleftrightarrow>")
+    ("|-->" . "\\<longmapsto>")
+    ("<-->" . "\\<longleftrightarrow>")
+    ("<<" . "\\<guillemotleft>")
+    (">>" . "\\<guillemotright>")
+    ("[|" . "\\<lbrakk>")
+    ("|]" . "\\<rbrakk>")
+    ("{|" . "\\<lbrace>")
+    ("|}" . "\\<rbrace>")
+    ("---" . "\\<emdash>")))
+
+(defcustom isar-shortcut-alist
+  (append
+   isar-symbol-shortcuts
+   ;; LaTeX-like syntax for symbol names, easier to type
+   (mapcar 
+    (lambda (tokentry)
+      (cons (concat "\\" (car tokentry))
+	    (format isar-token-format (car tokentry))))
+    (append isar-greek-letters-tokens isar-symbols-tokens)))
+  "Shortcut key sequence table for token input.
 
 You can adjust this table to add more entries, or to change entries for
 glyphs that not are available in your Emacs or chosen font.
 
 These shortcuts are only used for input; no reverse conversion is
-performed.  But if tokens exist for the target of shortcuts, they
-will be used on saving the buffer."
+performed.  "
   :type '(repeat (cons (string :tag "Shortcut sequence")
 		       (string :tag "Unicode string")))
   :set 'proof-set-value
@@ -589,9 +556,9 @@ will be used on saving the buffer."
 
 (eval-after-load "isar" 
   '(setq 
-    proof-xsym-activate-command
+    proof-tokens-activate-command
     (isar-markup-ml "change print_mode (insert (op =) \"xsymbols\")")
-    proof-xsym-deactivate-command
+    proof-tokens-deactivate-command
     (isar-markup-ml "change print_mode (remove (op =) \"xsymbols\")")))
 
 
diff --git a/isar/isar.el b/isar/isar.el
index e3ac984c..b05b359c 100644
--- a/isar/isar.el
+++ b/isar/isar.el
@@ -58,7 +58,7 @@ See -k option for Isabelle interface script."
 
 (eval-after-load "pg-custom"
   '(setq isar-toolbar-entries
-	 (remassoc 'qed (remassoc 'goal isar-toolbar-entries))))
+	 (assq-delete-all 'qed (assq-delete-all 'goal isar-toolbar-entries))))
 
 
 (defun isar-strip-terminators ()
@@ -104,8 +104,7 @@ See -k option for Isabelle interface script."
    proof-string-start-regexp    isar-string-start-regexp
    proof-string-end-regexp      isar-string-end-regexp
 
-   ;; Next few used for func-menu and recognizing goal..save regions in
-   ;; script buffer.
+   ;; For func-menu and finding goal..save regions
    proof-save-command-regexp    isar-save-command-regexp
    proof-goal-command-regexp    isar-goal-command-regexp
    proof-goal-with-hole-regexp  isar-named-entity-regexp
@@ -188,15 +187,15 @@ See -k option for Isabelle interface script."
    ;; matches names of assumptions
    proof-shell-assumption-regexp        isar-id
 
-   proof-shell-start-goals-regexp       "\366\n\\|\^AO\n"
-   proof-shell-end-goals-regexp         "\367\\|\^AP"
+   proof-shell-start-goals-regexp       "\^AO\n"
+   proof-shell-end-goals-regexp         "\^AP"
 
    proof-shell-init-cmd			nil
    proof-shell-restart-cmd              "ProofGeneral.restart"
 
    proof-shell-eager-annotation-start-length 2
-   proof-shell-eager-annotation-start   "\360\\|\362\\|\^AI\\|\^AK"
-   proof-shell-eager-annotation-end     "\361\\|\363\\|\^AJ\\|\^AL"
+   proof-shell-eager-annotation-start   "\^AI\\|\^AK"
+   proof-shell-eager-annotation-end     "\^AJ\\|\^AL"
 
    ;; Isabelle is learning to talk PGIP...
    proof-shell-match-pgip-cmd		"<pgip"
@@ -215,11 +214,6 @@ See -k option for Isabelle interface script."
      (string  "term \"%s\";")
      (comment "term \"%s\";"))
 
-   ;; Allow font-locking for output based on hidden annotations, see
-   ;; isar-output-font-lock-keywords-1
-   pg-use-specials-for-fontify		t
-   pg-after-fontify-output-hook	        'pg-remove-specials
-
    pg-special-char-regexp
    (if proof-shell-unicode "
[0-9A-Z]"
      ;; next string could be: "[\350-\377]", but that's buggy with XEmacs 21.5 (beta)
@@ -345,14 +339,15 @@ proof-shell-retract-files-regexp."
 
 (defpgdefault menu-entries
   (append
-   (list isabelle-logics-menu)
+   (list isabelle-logics-menu-entries)
    (list
     (cons "Commands"
           (list
            ["refute"             isar-cmd-refute         t]
            ["quickcheck"         isar-cmd-quickcheck     t]
            ["sledgehammer"       isar-cmd-sledgehammer   t]
-	   ["display draft"	 isar-cmd-display-draft  t])))
+	   ["display draft"	 isar-cmd-display-draft  t]
+	   ["set isatool"        (isa-set-isatool-command 't) t])))
    (list
     (cons "Show me ..."
           (list
@@ -372,6 +367,8 @@ proof-shell-retract-files-regexp."
            ["inner syntax"       isar-help-syntax         t]
            ["methods"            isar-help-methods        t])))))
 
+(defpgdefault help-menu-entries isabelle-docs-menu)
+
 ;; undo proof commands
 (defun isar-count-undos (span)
   "Count number of undos SPAN, return command needed to undo that far."
@@ -509,12 +506,14 @@ Checks the width in the `proof-goals-buffer'"
            (let ((current-width
                   ;; Actually, one might want the width of the
                   ;; proof-response-buffer instead. Never mind.
-                  (max 20 (window-width (get-buffer-window proof-goals-buffer t)))))
+                  (max 20 (window-width 
+			   (get-buffer-window proof-goals-buffer t)))))
 
              (if (equal current-width isar-shell-current-line-width) ()
                (setq isar-shell-current-line-width current-width)
                (set-buffer proof-shell-buffer)
-               (setq ans (format "pretty_setmargin %d;" (- current-width 4)))))))
+               (setq ans (format "pretty_setmargin %d;" 
+				 (- current-width 4)))))))
     ans))
 
 ;;
@@ -547,43 +546,32 @@ Checks the width in the `proof-goals-buffer'"
 (defun isar-mode-config ()
   (isar-mode-config-set-variables)
   (isar-init-syntax-table)
-  (setq font-lock-keywords isar-font-lock-keywords-1)
-  (setq comment-quote-nested nil) ;; can cope with nested comments
+  (setq proof-script-font-lock-keywords isar-font-lock-keywords-1)
+  (set (make-local-variable 'comment-quote-nested) nil) ;; can cope with nested comments
   (set (make-local-variable 'outline-regexp) isar-outline-regexp)
   (set (make-local-variable 'outline-heading-end-regexp) isar-outline-heading-end-regexp)
-  (setq blink-matching-paren-dont-ignore-comments t)
+  (set (make-local-variable 'blink-matching-paren-dont-ignore-comments) t)
   (add-hook 'proof-shell-insert-hook 'isar-preprocessing)
   (proof-config-done))
 
 (defun isar-shell-mode-config ()
   "Configure Proof General proof shell for Isabelle/Isar."
   (isar-init-output-syntax-table)
-  (setq font-lock-keywords
-	(append
-	 isar-output-font-lock-keywords-1
-	 (if (boundp 'x-symbol-isar-font-lock-keywords)
-	     x-symbol-isar-font-lock-keywords)))
   (isar-shell-mode-config-set-variables)
   (proof-shell-config-done))
 
 (defun isar-response-mode-config ()
   (isar-init-output-syntax-table)
-  (setq font-lock-keywords
-	(append
-	 isar-output-font-lock-keywords-1
-	 (if isar-x-symbol-enable
-	     x-symbol-isar-font-lock-keywords)))
+  (setq proof-response-font-lock-keywords 
+	isar-output-font-lock-keywords-1)
   (proof-response-config-done))
 
 (defun isar-goals-mode-config ()
   (setq pg-goals-change-goal "prefer %s")
   (setq pg-goals-error-regexp proof-shell-error-regexp)
   (isar-init-output-syntax-table)
-  (setq font-lock-keywords
-	(append
-	 isar-goals-font-lock-keywords
-	 (if isar-x-symbol-enable
-	     x-symbol-isar-font-lock-keywords)))
+  (setq proof-goals-font-lock-keywords
+	 isar-goals-font-lock-keywords)
   (proof-goals-config-done))
 
 (defun isar-goalhyplit-test ()
diff --git a/isar/x-symbol-isar.el b/isar/x-symbol-isar.el
deleted file mode 100644
index 6a8a8fbf..00000000
--- a/isar/x-symbol-isar.el
+++ /dev/null
@@ -1,517 +0,0 @@
-;; x-symbol-isar.el   
-;; Token language "Isabelle Symbols" for package x-symbol
-;;
-;;  ID:         $Id$
-;;  Author:     David von Oheimb
-;;              Updates by Markus Wenzel, Christoph Wedler, David Aspinall.
-;;  Copyright   1998 Technische Universitaet Muenchen
-;;  License     GPL (GNU GENERAL PUBLIC LICENSE)
-;;
-;; This file is part of the Proof General distribution.
-
-(eval-when-compile
-  (require 'cl))			; to properly compile 'block'
-
-(defvar x-symbol-isar-required-fonts nil)
-
-;;;===========================================================================
-;;;  General language accesses, see `x-symbol-language-access-alist'
-;;;===========================================================================
-
-;; NB da: these next two are also set in proof-x-symbol.el, but
-;; it would be handy to be able to use this file away from PG.  
-(defvar x-symbol-isar-name "Isabelle Symbol")
-(defvar x-symbol-isar-modeline-name "isa")
-
-(defcustom x-symbol-isar-header-groups-alist nil
-   "*If non-nil, used in isasym specific grid/menu.
-See `x-symbol-header-groups-alist'."
-  :group 'x-symbol-isar
-  :group 'x-symbol-input-init
-  :type 'x-symbol-headers)
-
-(defcustom x-symbol-isar-electric-ignore 
-  "[:'][A-Za-z]\\|<=\\|\\[\\[\\|\\]\\]\\|~="
-  "*Additional Isabelle version of `x-symbol-electric-ignore'."
-  :group 'x-symbol-isar
-  :group 'x-symbol-input-control
-  :type 'x-symbol-function-or-regexp)
-
-
-(defvar x-symbol-isar-required-fonts nil
-  "List of features providing fonts for language `isabelle'.")
-
-(defvar x-symbol-isar-extra-menu-items nil
-  "Extra menu entries for language `isabelle'.")
-
-
-(defvar x-symbol-isar-token-grammar
-  '(x-symbol-make-grammar
-    :encode-spec (((t . "\\\\")))
-    :decode-regexp "\\\\+<[A-Za-z]+>"
-    :input-spec nil
-    :token-list x-symbol-isar-token-list))
-
-(defun x-symbol-isar-token-list (tokens)
-  (mapcar (lambda (x) (cons x t)) tokens))
-
-(defvar x-symbol-isar-user-table nil
-  "User table defining Isabelle commands, used in `x-symbol-isar-table'.")
-
-(defvar x-symbol-isar-generated-data nil
-  "Internal.")
-
-
-;;;===========================================================================
-;;;  No image support
-;;;===========================================================================
-
-(defvar x-symbol-isar-master-directory  'ignore)
-(defvar x-symbol-isar-image-searchpath '("./"))
-(defvar x-symbol-isar-image-cached-dirs '("images/" "pictures/"))
-(defvar x-symbol-isar-image-file-truename-alist nil)
-(defvar x-symbol-isar-image-keywords nil)
-
-
-;;;===========================================================================
-;;  super- and subscripts
-;;;===========================================================================
-
-;; one char: \<^sup>, \<^sub>, \<^isub>, and \<^isup>
-;; spanning: \<^bsup>...\<^esup> and \<^bsub>..\<^esub>
-
-(defcustom x-symbol-isar-subscript-matcher 'x-symbol-isar-subscript-matcher
-  "Function matching super-/subscripts for language `isa'.
-See language access `x-symbol-LANG-subscript-matcher'."
-  :group 'x-symbol-isar
-  :type 'function)
-
-(defcustom x-symbol-isar-font-lock-regexp "\\\\<\\^[ib]?su[bp]>"
-  "Regexp matching the start tag of Isabelle super- and subscripts."
-  :group 'x-symbol-isar
-  :type 'regexp)
-
-(defcustom x-symbol-isar-font-lock-limit-regexp "\n\\|\\\\<\\^[be]su[bp]>"
-  "Regexp matching the end of line and the start and end tags of Isabelle
-spanning super- and subscripts."
-  :group 'x-symbol-isar
-  :type 'regexp)
-
-(defcustom x-symbol-isar-font-lock-contents-regexp "."
-  "*Regexp matching the spanning super- and subscript contents.
-This regexp should match the text between the opening and closing super-
-or subscript tag."
-  :group 'x-symbol-isar  
-  :type 'regexp)
-
-
-;; the [\350-\357].\350\\|\^A[A-H].\^AA part is there to enable single
-;; char sub/super scripts with coloured Isabelle output.
-(defcustom x-symbol-isar-single-char-regexp 
-  "\\([^\\]\\|\\\\<[A-Za-z]+>\\)\\|[\350-\357]\\([^\\]\\|\\\\<[A-Za-z]+>\\)\350\\|\^A[A-H]\\([^\\]\\|\\\\<[A-Za-z]+>\\)\^AA"
-  "Return regexp matching \<ident> or c for some char c."
-  :group 'x-symbol-isar
-  :type 'regexp)
-
-(defun x-symbol-isar-subscript-matcher (limit)  
-  (block nil
-    (let (open-beg open-end close-end close-beg script-type)
-      (while (re-search-forward x-symbol-isar-font-lock-regexp limit t)
-        (setq open-beg (match-beginning 0)
-              open-end (match-end 0)
-              script-type (if (eq (char-after (- open-end 2)) ?b)
-                              'x-symbol-sub-face
-                           'x-symbol-sup-face))
-	(when (not (proof-string-match "[ \t\n]" (string (char-after open-end))))
-	  (if (eq (char-after (- open-end 5)) ?b) ; if is spanning sup-/subscript
-	      (let ((depth 1)) ; level of nesting
-		(while (and (not (eq depth 0))
-			    (re-search-forward x-symbol-isar-font-lock-limit-regexp
-					       limit 'limit))
-		  (setq close-beg (match-beginning 0)
-			close-end (match-end 0))
-		  (if (eq (char-after (- close-end 1)) ?\n) ; if eol
-		      (setq depth 0)
-		    (if (eq (char-after (- close-end 5)) ?b) ; if end of span
-			(setq depth (+ depth 1))
-		      (setq depth (- depth 1)))))
-		(when (eq depth 0)
-		  (when
-		      (save-excursion
-			(goto-char open-end)
-			(re-search-forward x-symbol-isar-font-lock-contents-regexp
-					   close-beg t))
-		    (store-match-data (list open-beg close-end
-					    open-beg open-end
-					    open-end close-beg
-					    close-beg close-end))
-		    (return script-type)))
-		(goto-char close-beg))
-	    (when (re-search-forward x-symbol-isar-single-char-regexp
-				     limit 'limit)
-	      (setq close-end (match-end 0))
-	      (store-match-data (list open-beg close-end
-				      open-beg open-end
-				      open-end close-end))
-	      (return script-type))))))))
-   
-(defun isabelle-match-subscript (limit)
-  (if isar-x-symbol-enable
-      (setq x-symbol-isar-subscript-type
-            (funcall x-symbol-isar-subscript-matcher limit))))
-
-;; these are used for Isabelle output only. x-symbol does its own
-;; setup of font-lock-keywords for the theory buffer
-;; (x-symbol-isar-font-lock-keywords does not belong to language
-;; access any more)
-(defvar x-symbol-isar-font-lock-keywords
-  '((isabelle-match-subscript
-     (1 x-symbol-invisible-face t)
-     (2 (progn x-symbol-isar-subscript-type) prepend)
-     (3 x-symbol-invisible-face t t)))
-  "Isabelle font-lock keywords for super- and subscripts.")
-
-(defvar x-symbol-isar-font-lock-allowed-faces t)
-
-
-;;;===========================================================================
-;;;  Charsym Info
-;;;===========================================================================
-
-(defcustom x-symbol-isar-class-alist
-  '((VALID "Isabelle Symbol" (x-symbol-info-face))
-    (INVALID "no Isabelle Symbol" (red x-symbol-info-face)))
-  "Alist for Isabelle's token classes displayed by info in echo area.
-See `x-symbol-language-access-alist' for details."
-  :group 'x-symbol-texi
-  :group 'x-symbol-info-strings
-;;  :set 'x-symbol-set-cache-variable   [causes compile error]
-  :type 'x-symbol-class-info)
-
-
-(defcustom x-symbol-isar-class-face-alist nil
-  "Alist for Isabelle's color scheme in TeXinfo's grid and info.
-See `x-symbol-language-access-alist' for details."
-  :group 'x-symbol-isar
-  :group 'x-symbol-input-init
-  :group 'x-symbol-info-general
-;;  :set 'x-symbol-set-cache-variable   [causes compile error]
-  :type 'x-symbol-class-faces)
-
-
-
-;;;===========================================================================
-;;;  The tables
-;;;===========================================================================
-
-(defvar x-symbol-isar-case-insensitive nil)
-(defvar x-symbol-isar-token-shape nil)
-(defvar x-symbol-isar-input-token-ignore nil)
-(defvar x-symbol-isar-token-list 'identity)
-
-(defvar x-symbol-isar-symbol-table      ; symbols (isabelle font)
-  '((visiblespace "\\<spacespace>")
-    (Gamma "\\<Gamma>")
-    (Delta "\\<Delta>")
-    (Theta "\\<Theta>")
-    (Lambda "\\<Lambda>")
-    (Pi "\\<Pi>")
-    (Sigma "\\<Sigma>")
-    (Phi "\\<Phi>")
-    (Psi "\\<Psi>")
-    (Omega "\\<Omega>")
-    (alpha "\\<alpha>")
-    (beta "\\<beta>")
-    (gamma "\\<gamma>")
-    (delta "\\<delta>")
-    (epsilon1 "\\<epsilon>")
-    (zeta "\\<zeta>")
-    (eta "\\<eta>")
-    (theta "\\<theta>")
-    (kappa1 "\\<kappa>")
-    (lambda "\\<lambda>")
-    (mu "\\<mu>")
-    (nu "\\<nu>")
-    (xi "\\<xi>")
-    (pi "\\<pi>")
-    (rho1 "\\<rho>")
-    (sigma "\\<sigma>")
-    (tau "\\<tau>")
-    (phi1 "\\<phi>")
-    (chi "\\<chi>")
-    (psi "\\<psi>")
-    (omega "\\<omega>")
-    (notsign "\\<not>")
-    (logicaland "\\<and>")
-    (logicalor "\\<or>")
-    (universal1 "\\<forall>")
-    (existential1 "\\<exists>")
-    (epsilon "\\<some>")
-    (biglogicaland "\\<And>")
-    (ceilingleft "\\<lceil>")
-    (ceilingright "\\<rceil>")
-    (floorleft "\\<lfloor>")
-    (floorright "\\<rfloor>")
-    (bardash "\\<turnstile>")
-    (bardashdbl "\\<Turnstile>")
-    (semanticsleft "\\<lbrakk>")
-    (semanticsright "\\<rbrakk>")
-    (periodcentered "\\<cdot>")
-    (element "\\<in>")
-    (reflexsubset "\\<subseteq>")
-    (intersection "\\<inter>")
-    (union "\\<union>")
-    (bigintersection "\\<Inter>")
-    (bigunion "\\<Union>")
-    (sqintersection "\\<sqinter>")
-    (squnion "\\<squnion>")
-    (bigsqintersection "\\<Sqinter>")
-    (bigsqunion "\\<Squnion>")
-    (perpendicular "\\<bottom>")
-    (dotequal "\\<doteq>")
-    (wrong "\\<wrong>")
-    (equivalence "\\<equiv>")
-    (notequal "\\<noteq>")
-    (propersqsubset "\\<sqsubset>")
-    (reflexsqsubset "\\<sqsubseteq>")
-    (properprec "\\<prec>")
-    (reflexprec "\\<preceq>")
-    (propersucc "\\<succ>")
-    (approxequal "\\<approx>")
-    (similar "\\<sim>")
-    (simequal "\\<simeq>")
-    (lessequal "\\<le>")
-    (coloncolon "\\<Colon>")
-    (arrowleft "\\<leftarrow>")
-    (endash "\\<midarrow>")
-    (arrowright "\\<rightarrow>")
-    (arrowdblleft "\\<Leftarrow>")
-;   (nil "\\<Midarrow>")
-    (arrowdblright "\\<Rightarrow>")
-    (frown "\\<frown>")
-    (mapsto "\\<mapsto>")
-    (leadsto "\\<leadsto>")
-    (arrowup "\\<up>")
-    (arrowdown "\\<down>")
-    (notelement "\\<notin>")
-    (multiply "\\<times>")
-    (circleplus "\\<oplus>")
-    (circleminus "\\<ominus>")
-    (circlemultiply "\\<otimes>")
-    (circleslash "\\<oslash>")
-    (propersubset "\\<subset>")
-    (infinity "\\<infinity>")
-    (box "\\<box>")
-    (lozenge1 "\\<diamond>")
-    (circ "\\<circ>")
-    (bullet "\\<bullet>")
-    (bardbl "\\<parallel>")
-    (radical "\\<surd>")
-    (copyright "\\<copyright>")))
-
-(defvar x-symbol-isar-xsymbol-table    ; xsymbols
-  '((Xi "\\<Xi>")
-    (Upsilon1 "\\<Upsilon>")
-    (iota "\\<iota>")
-    (upsilon "\\<upsilon>")
-    (plusminus "\\<plusminus>")
-    (division "\\<div>")
-    (longarrowright "\\<longrightarrow>")
-    (longarrowleft "\\<longleftarrow>")
-    (longarrowboth "\\<longleftrightarrow>")
-    (longarrowdblright "\\<Longrightarrow>")
-    (longarrowdblleft "\\<Longleftarrow>")
-    (longarrowdblboth "\\<Longleftrightarrow>")
-    (brokenbar "\\<bar>")
-    (hyphen "\\<hyphen>")
-    (macron "\\<inverse>")
-    (exclamdown "\\<exclamdown>")
-    (questiondown "\\<questiondown>")
-    (guillemotleft "\\<guillemotleft>")
-    (guillemotright "\\<guillemotright>")
-    (degree "\\<degree>")
-    (onesuperior "\\<onesuperior>")
-    (onequarter "\\<onequarter>")
-    (twosuperior "\\<twosuperior>")
-    (onehalf "\\<onehalf>")
-    (threesuperior "\\<threesuperior>")
-    (threequarters "\\<threequarters>")
-    (paragraph "\\<paragraph>")
-    (registered "\\<registered>")
-    (ordfeminine "\\<ordfeminine>")
-    (masculine "\\<ordmasculine>")
-    (section "\\<section>")
-    (sterling "\\<pounds>")
-    (yen "\\<yen>")
-    (cent "\\<cent>")
-    (currency "\\<currency>")
-    (braceleft2 "\\<lbrace>")
-    (braceright2 "\\<rbrace>")
-    (top "\\<top>")
-    (congruent "\\<cong>")
-    (club "\\<clubsuit>")
-    (diamond "\\<diamondsuit>")
-    (heart "\\<heartsuit>")
-    (spade "\\<spadesuit>")
-    (arrowboth "\\<leftrightarrow>")
-    (greaterequal "\\<ge>")
-    (proportional "\\<propto>")
-    (partialdiff "\\<partial>")
-    (ellipsis "\\<dots>")
-    (aleph "\\<aleph>")
-    (Ifraktur "\\<Im>")
-    (Rfraktur "\\<Re>")
-    (weierstrass "\\<wp>")
-    (emptyset "\\<emptyset>")
-    (angle "\\<angle>")
-    (gradient "\\<nabla>")
-    (product "\\<Prod>")
-    (arrowdblboth "\\<Leftrightarrow>")
-    (arrowdblup "\\<Up>")
-    (arrowdbldown "\\<Down>")
-    (angleleft "\\<langle>")
-    (angleright "\\<rangle>")
-    (summation "\\<Sum>")
-    (integral "\\<integral>")
-    (circleintegral "\\<ointegral>")
-    (dagger "\\<dagger>")
-    (sharp "\\<sharp>")
-    (star "\\<star>")
-    (smltriangleright "\\<triangleright>")
-    (triangleleft "\\<lhd>")
-    (triangle "\\<triangle>")
-    (triangleright "\\<rhd>")
-    (trianglelefteq "\\<unlhd>")
-    (trianglerighteq "\\<unrhd>")
-    (smltriangleleft "\\<triangleleft>")
-    (natural "\\<natural>")
-    (flat "\\<flat>")
-    (amalg "\\<amalg>")
-    (Mho "\\<mho>")
-    (arrowupdown "\\<updown>")
-    (longmapsto "\\<longmapsto>")
-    (arrowdblupdown "\\<Updown>")
-    (hookleftarrow "\\<hookleftarrow>")
-    (hookrightarrow "\\<hookrightarrow>")
-    (rightleftharpoons "\\<rightleftharpoons>")
-    (leftharpoondown "\\<leftharpoondown>")
-    (rightharpoondown "\\<rightharpoondown>")
-    (leftharpoonup "\\<leftharpoonup>")
-    (rightharpoonup "\\<rightharpoonup>")
-    (asym "\\<asymp>")
-    (minusplus "\\<minusplus>")
-    (bowtie "\\<bowtie>")
-    (centraldots "\\<cdots>")
-    (circledot "\\<odot>")
-    (propersuperset "\\<supset>")
-    (reflexsuperset "\\<supseteq>")
-    (propersqsuperset "\\<sqsupset>")
-    (reflexsqsuperset "\\<sqsupseteq>")
-    (lessless "\\<lless>")
-    (greatergreater "\\<ggreater>")
-    (unionplus "\\<uplus>")
-    (backslash3 "\\<setminus>")
-    (smile "\\<smile>")
-    (reflexsucc "\\<succeq>")
-    (dashbar "\\<stileturn>")
-    (biglogicalor "\\<Or>")
-    (bigunionplus "\\<Uplus>")
-    (daggerdbl "\\<ddagger>")
-    (bigbowtie "\\<Join>")
-    (booleans "\\<bool>")
-    (complexnums "\\<complex>")
-    (natnums "\\<nat>")
-    (rationalnums "\\<rat>")
-    (realnums "\\<real>")
-    (integers "\\<int>")
-    (lesssim "\\<lesssim>")
-    (greatersim "\\<greatersim>")
-    (lessapprox "\\<lessapprox>")
-    (greaterapprox "\\<greaterapprox>")
-    (definedas "\\<triangleq>")
-    (cataleft "\\<lparr>")
-    (cataright "\\<rparr>")
-    (bigcircledot "\\<Odot>")
-    (bigcirclemultiply "\\<Otimes>")
-    (bigcircleplus "\\<Oplus>")
-    (coproduct "\\<Coprod>")
-    (cedilla "\\<cedilla>")
-    (diaeresis "\\<dieresis>")
-    (acute "\\<acute>")
-    (hungarumlaut "\\<hungarumlaut>")
-    (lozenge "\\<lozenge>")
-    (smllozenge "\\<struct>")
-    (dotlessi "\\<index>")
-    (euro "\\<euro>")
-    (zero1 "\\<zero>")
-    (one1 "\\<one>")
-    (two1 "\\<two>")
-    (three1 "\\<three>")
-    (four1 "\\<four>")
-    (five1 "\\<five>")
-    (six1 "\\<six>")
-    (seven1 "\\<seven>")
-    (eight1 "\\<eight>")
-    (nine1 "\\<nine>")
-    ))
-
-(defun x-symbol-isar-prepare-table (table)
-  "Prepare table for Isabelle/Isar."
-  (mapcar (lambda (entry)
-	    (list (car entry) nil
-		  (cadr entry) 
-		  (concat "\\" (cadr entry))))
-	  table))
-
-(defvar x-symbol-isar-table
-  (x-symbol-isar-prepare-table
-   (append
-    x-symbol-isar-user-table
-    x-symbol-isar-symbol-table
-    x-symbol-isar-xsymbol-table)))
-
-
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;
-;; User-level settings for X-Symbol 
-;;
-;; this is MODE-ON CODING 8BITS UNIQUE SUBSCRIPTS IMAGE
-(defcustom x-symbol-isar-auto-style
-  '(isar-x-symbol-enable	   ; MODE-ON: whether to turn on interactively
-    nil   ;; x-symbol-coding
-    'null ;; x-symbol-8bits	   [NEVER want it; null disables search]
-    nil   ;; x-symbol-unique
-    t     ;; x-symbol-subscripts
-    nil)  ;; x-symbol-image
-  "Variable used to document a language access.
-See documentation of `x-symbol-auto-style'."
-  :group 'x-symbol-isar
-  :group 'x-symbol-mode
-  :type 'x-symbol-auto-style)
-
-;; FIXME da: is this needed?
-(defcustom x-symbol-isar-auto-coding-alist nil
-  "*Alist used to determine the file coding of ISABELLE buffers.
-Used in the default value of `x-symbol-auto-mode-alist'.  See
-variable `x-symbol-auto-coding-alist' for details."
-  :group 'x-symbol-isar
-  :group 'x-symbol-mode
-  :type 'x-symbol-auto-coding)
-
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;
-;; x-symbol support
-;;
-;; The following settings configure the generic PG package.
-;;
-
-(eval-after-load "isar" ;; allow use outside PG
-  '(setq 
-    proof-xsym-activate-command
-    (isar-markup-ml "change print_mode (insert (op =) \"xsymbols\")")
-    proof-xsym-deactivate-command
-    (isar-markup-ml "change print_mode (remove (op =) \"xsymbols\")")))
-
-(provide 'x-symbol-isar)