1826
|
1 |
#!/bin/bash
|
|
2 |
################################################
|
|
3 |
# Title: Tools/8bit/xemacs/isa_xemacs
|
|
4 |
# ID: $Id$
|
|
5 |
# Author: Franz Regensburger
|
|
6 |
# Copyright 1995 TU Muenchen
|
|
7 |
#
|
|
8 |
# isa_xemacs -- xemacs for Isabelle environment
|
|
9 |
#
|
|
10 |
# Franz Regensburger <regensbu@informatik.tu-muenchen.de> 22.3.95
|
|
11 |
#
|
|
12 |
###############################################
|
|
13 |
#
|
|
14 |
# The script `isa_xemacs' opens the XEmacs editor with the special
|
|
15 |
# 8bit font for Isabelle. It also provides keyboard bindings for the
|
|
16 |
# access to the graphical characters.
|
|
17 |
#
|
|
18 |
# The script is configured by the master makefile ../Makefile and
|
|
19 |
# the perl script ../bin/gen-isa_xemacs which reads the configuration file
|
|
20 |
# ../config/key-table.inp. Edit these files to make changes!
|
|
21 |
#
|
|
22 |
####################################################
|
|
23 |
# do not configure macros below, use master Makefile
|
|
24 |
####################################################
|
|
25 |
|
|
26 |
# emacs command name. Name of your emacs executable
|
|
27 |
ENAME=xemacs
|
|
28 |
|
|
29 |
#users init file ($HOME is added). This file is loaded after
|
|
30 |
#the init file $PREFIX.emacs
|
1907
|
31 |
INIT=.emacs_xemacs_isa
|
1826
|
32 |
|
|
33 |
###############################################
|
|
34 |
# do not edit below
|
|
35 |
###############################################
|
|
36 |
|
|
37 |
# prefix of init file and title of emacs window
|
|
38 |
PREFIX=isa_xemacs
|
|
39 |
|
|
40 |
# Name of the directory where this file is located
|
|
41 |
EDIR=xemacs
|
|
42 |
|
|
43 |
# emacs init file for Isabelle
|
|
44 |
INITFILE=$ISABELLE8BIT/$EDIR/$PREFIX.emacs
|
|
45 |
|
|
46 |
# set font as XResource
|
|
47 |
# needed for versions later than LEmacs 19.9
|
|
48 |
echo "$PREFIX*default.attributeFont: isacr14" | xrdb -merge - >/dev/null
|
|
49 |
|
|
50 |
# pop up isabelle emacs
|
|
51 |
$ENAME \
|
|
52 |
-title "$PREFIX" \
|
|
53 |
-name "$PREFIX" \
|
|
54 |
-l $INITFILE -l "$HOME/$INIT"\
|
|
55 |
$* 2>/dev/null
|
|
56 |
|