diff options
| -rw-r--r-- | isar/Example.thy | 1 | ||||
| -rw-r--r-- | isar/interface | 11 | ||||
| -rw-r--r-- | isar/isar.el | 11 | ||||
| -rw-r--r-- | x-symbol/etc/fonts/Makefile | 14 | ||||
| -rw-r--r-- | x-symbol/lisp/x-symbol-vars.el | 9 |
5 files changed, 38 insertions, 8 deletions
diff --git a/isar/Example.thy b/isar/Example.thy index c86bf89a..278e5964 100644 --- a/isar/Example.thy +++ b/isar/Example.thy @@ -19,6 +19,7 @@ proof qed qed +asd text {* Proper proof text -- \textit{advanced version}. *} diff --git a/isar/interface b/isar/interface index 9f2d33a6..a562f41e 100644 --- a/isar/interface +++ b/isar/interface @@ -30,6 +30,7 @@ usage() echo " -P BOOL actually start Proof General (default true), otherwise" echo " run plain tty session" echo " -X BOOL configure the X-Symbol package on startup (default true)" + echo " -f SIZE set X-Symbol font size (default 14)" echo " -g GEOMETRY specify Emacs geometry" echo " -k NAME use specific isar-keywords for named logic" echo " -l NAME logic image name (default \$ISABELLE_LOGIC=$ISABELLE_LOGIC)" @@ -68,11 +69,12 @@ INITFILE="true" WINDOWSYSTEM="true" XSYMBOL="" XSYMBOLSETUP=true +XSYMBOL_FONTSIZE="12" getoptions() { OPTIND=1 - while getopts "I:P:X:g:k:l:m:p:u:w:x:" OPT + while getopts "I:P:X:f:g:k:l:m:p:u:w:x:" OPT do case "$OPT" in I) @@ -84,6 +86,9 @@ getoptions() X) XSYMBOLSETUP="$OPTARG" ;; + f) + XSYMBOL_FONTSIZE="$OPTARG" + ;; g) GEOMETRY="$OPTARG" ;; @@ -229,8 +234,8 @@ else PROOFGENERAL_XSYMBOL="$XSYMBOL" export PROOFGENERAL_HOME PROOFGENERAL_ASSISTANTS PROOFGENERAL_LOGIC PROOFGENERAL_XSYMBOL - export ISABELLE_OPTIONS + export ISABELLE_OPTIONS XSYMBOL_FONTSIZE eval exec "$PROGNAME" "$ARGS" "$FILES" -fi +fi
\ No newline at end of file diff --git a/isar/isar.el b/isar/isar.el index 66f5d8ad..523cab31 100644 --- a/isar/isar.el +++ b/isar/isar.el @@ -352,6 +352,16 @@ proof-shell-retract-files-regexp." ;;; help menu ;;; +(setq find-rewrites-command "find_rewrites \"%s\"") + +(proof-define-assistant-command-witharg isar-help-rewrites + "Search for rewrite rules matching given term." + find-rewrites-command + "Find rewrite rules matching" + (proof-shell-invisible-command arg)) + +(define-key (proof-ass keymap) [h R] 'isar-help-rewrites) + ;;; da: how about a `C-c C-a h ?' for listing available keys? ;;; NB: definvisible must come after derived modes because uses @@ -394,6 +404,7 @@ proof-shell-retract-files-regexp." ["cases" isar-help-cases t] ["facts" isar-help-facts t] ["matching rules" isar-help-intro-rules t] + ["matching rewrites" isar-help-rewrites t] ["term bindings" isar-help-binds t] "----" ["classical rules" isar-help-claset t] diff --git a/x-symbol/etc/fonts/Makefile b/x-symbol/etc/fonts/Makefile index 55c047fd..7ed9f1ee 100644 --- a/x-symbol/etc/fonts/Makefile +++ b/x-symbol/etc/fonts/Makefile @@ -1,7 +1,10 @@ ### Makefile --- create fonts for package x-symbol +# This version modified by Clemens Ballarin to accommodate 18pt and 24pt +# x-symb fonts. 23 April 2004 + ## Author: Christoph Wedler <wedler@users.sourceforge.net> -## Version: 4.5 +## Version: 4.4 ## Keywords: fonts, WYSIWYG, LaTeX, HTML, wp, math ## X-URL: http://x-symbol.sourceforge.net/ @@ -37,11 +40,13 @@ GENFONTS = ../genfonts ORIGFONTS = ../origfonts PCFDIR = ../pcf -ORIGBDFS = helvR12.bdf helvR14.bdf +ORIGBDFS = helvR12.bdf helvR14.bdf helvR18.bdf helvR24.bdf BDFS = 2helvR12.bdf 3helvR12.bdf 5etl14.bdf heriR12.bdf \ xsymb0_12.bdf xsymb1_12.bdf \ 2helvR14.bdf 3helvR14.bdf 5etl16.bdf heriR14.bdf \ - xsymb0_14.bdf xsymb1_14.bdf + xsymb0_14.bdf xsymb1_14.bdf \ + xsymb0_18.bdf xsymb1_18.bdf \ + xsymb0_24.bdf xsymb1_24.bdf EXTRABDFS = nilxs.bdf .SUFFIXES: @@ -79,7 +84,8 @@ echo: mkdirs: -if [ ! -d $(GENFONTS) ]; then mkdir $(GENFONTS); fi - -if [ ! -d $(PCFDIR) ]; then mkdir $(PCFDIR); fi + -if [ ! -d $(PCFDIR) ]; then mkdir $(PCFDIR); \ + else rm -f $(PCFDIR)/*.pcf ; fi; gens: $(GENS) diff --git a/x-symbol/lisp/x-symbol-vars.el b/x-symbol/lisp/x-symbol-vars.el index ac020879..e3e3b08f 100644 --- a/x-symbol/lisp/x-symbol-vars.el +++ b/x-symbol/lisp/x-symbol-vars.el @@ -1619,7 +1619,14 @@ encoding `x-symbol-default-coding' in this case. If nil, tokens are not decoded if they require the missing font. Values other than nil are safe, but latin characters without correct fonts will look strange.") -(defvar x-symbol-font-sizes '(("\\`-etl-" 16 14) ("" 14 12))) +(defvar x-symbol-font-sizes + (let ((env-fontsize (getenv "XSYMBOL_FONTSIZE"))) + (if (equal env-fontsize "14") '(("" 14 12)) + (if (equal env-fontsize "18") '(("" 18 14)) + (if (equal env-fontsize "24") '(("" 24 18)) + '(("\\`-etl-" 16 14) ("" 14 12))))))) + +;; (defvar x-symbol-font-sizes '(("\\`-etl-" 16 14) ("" 14 12))) ;; '(14 ("\\`-etl-.+_su[bp]-" . 14) ("\\`-etl-" . 16) ("_su[bp]-" . 12))) (defvar x-symbol-font-lock-with-extra-props |