diff options
| author | David Aspinall | 2005-02-15 18:43:22 +0000 |
|---|---|---|
| committer | David Aspinall | 2005-02-15 18:43:22 +0000 |
| commit | 3ebd8547bc8c938bd50fd4876c1f72d46dccb83c (patch) | |
| tree | 7be86c1ee3b8e12ecfa01cdb02471806a455783d /isar | |
| parent | bfe9931a3bdb711015eadc3696822d7e76c01186 (diff) | |
Changes from Clemens Ballarin for large X-Symbol fonts
Diffstat (limited to 'isar')
| -rw-r--r-- | isar/Example.thy | 1 | ||||
| -rw-r--r-- | isar/interface | 11 | ||||
| -rw-r--r-- | isar/isar.el | 11 |
3 files changed, 20 insertions, 3 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] |