minor adaptions
authoroheimb
Fri Dec 13 18:32:07 1996 +0100 (1996-12-13)
changeset 23922fb9659d30ca
parent 2391 de76cee7a30c
child 2393 651fce76c86c
minor adaptions
src/Tools/8bit/Makefile
src/Tools/8bit/c-sources/a2isa/a2isa
src/Tools/8bit/c-sources/isa2latex/isa2latex
src/Tools/8bit/doc/Makefile
src/Tools/8bit/doc/manual.dvi
src/Tools/8bit/doc/manual.itex
src/Tools/8bit/fonts/isacb24.bdf
src/Tools/8bit/fonts/isacr14.bdf
src/Tools/8bit/isa-patches/HOL/add-HOL.cfg
src/Tools/8bit/isa-patches/HOL/clean-HOL.cfg
src/Tools/8bit/isa-patches/HOL/extract-HOL.cfg
src/Tools/8bit/isa-patches/HOLCF/Up3.p
src/Tools/8bit/isa-patches/HOLCF/add-HOLCF.cfg
src/Tools/8bit/isa-patches/HOLCF/clean-HOLCF.cfg
src/Tools/8bit/isa-patches/HOLCF/extract-HOLCF.cfg
src/Tools/8bit/xemacs/isa_xemacs
     1.1 --- a/src/Tools/8bit/Makefile	Fri Dec 13 18:25:45 1996 +0100
     1.2 +++ b/src/Tools/8bit/Makefile	Fri Dec 13 18:32:07 1996 +0100
     1.3 @@ -55,7 +55,7 @@
     1.4  CONFIGFILES = config/Makefile config/key-table.inp config/conv-tables.inp
     1.5  
     1.6  #path stem to isabelle source, used by patcher
     1.7 -STEM = /usr/stud/oheimb/isabelle/
     1.8 +STEM = /usr/wiss/oheimb/isabelle/
     1.9  
    1.10  ###############################################
    1.11  # configuration for configuration files in ./config
     2.1 Binary file src/Tools/8bit/c-sources/a2isa/a2isa has changed
     3.1 Binary file src/Tools/8bit/c-sources/isa2latex/isa2latex has changed
     4.1 --- a/src/Tools/8bit/doc/Makefile	Fri Dec 13 18:25:45 1996 +0100
     4.2 +++ b/src/Tools/8bit/doc/Makefile	Fri Dec 13 18:32:07 1996 +0100
     4.3 @@ -28,9 +28,7 @@
     4.4  
     4.5  fontdocfiles: $(FONTDOCFILES)
     4.6  
     4.7 -manual: manual.tex manual.dvi
     4.8 -
     4.9 -manual.tex: manual.itex
    4.10 +manual: manual.dvi
    4.11  
    4.12  clean:
    4.13  	rm -f *.aux *.log
     5.1 Binary file src/Tools/8bit/doc/manual.dvi has changed
     6.1 --- a/src/Tools/8bit/doc/manual.itex	Fri Dec 13 18:25:45 1996 +0100
     6.2 +++ b/src/Tools/8bit/doc/manual.itex	Fri Dec 13 18:32:07 1996 +0100
     6.3 @@ -413,7 +413,9 @@
     6.4  command line arguments. According to the configuration file, the perl script
     6.5  patches specific portions of the C source of the 
     6.6  converter in the directory \bt{\$ISABELLE8BIT/c-sources/isa2latex} and
     6.7 -calls the C compiler to generate a new binary for \bt{isa2latex}.
     6.8 +calls the C compiler to generate a new binary for \bt{isa2latex}\footnote{
     6.9 +The \bt{Makefile} uses the lexical analyzer \bt{flex}. Make sure that you
    6.10 +use a recent version of it.}.
    6.11  
    6.12  If you want to alter the keyboard bindings for the various editors and the
    6.13  terminal, you have to change the configuration file \bt{key-table.inp}. 
     7.1 --- a/src/Tools/8bit/fonts/isacb24.bdf	Fri Dec 13 18:25:45 1996 +0100
     7.2 +++ b/src/Tools/8bit/fonts/isacb24.bdf	Fri Dec 13 18:32:07 1996 +0100
     7.3 @@ -1,5 +1,5 @@
     7.4  STARTFONT 2.1
     7.5 -FONT spcb24
     7.6 +FONT isacb24
     7.7  SIZE 24 75 75
     7.8  FONTBOUNDINGBOX 16 22 6 -5
     7.9  STARTPROPERTIES 22
    7.10 @@ -18,9 +18,9 @@
    7.11  AVERAGE_WIDTH 150
    7.12  CHARSET_REGISTRY "ISO8859"
    7.13  CHARSET_ENCODING "1"
    7.14 -CHARSET_COLLECTIONS "ASCII ISO8859-1 ADOBE-STANDARD"
    7.15 -FULL_NAME "Courier Bold"
    7.16 -COPYRIGHT "Copyright (c)1985,1987 Adobe Systems, Inc., Portions Copyright 1988"
    7.17 +CHARSET_COLLECTIONS ""
    7.18 +FULL_NAME "Isabelle24 Bold"
    7.19 +COPYRIGHT "Copyright (c)1985,1987 Adobe Systems, Inc., Portions Copyright 1988, Portions Copyright 1995 TU Muenchen"
    7.20  FONT_ASCENT 17
    7.21  FONT_DESCENT 5
    7.22  CAP_HEIGHT 15
     8.1 --- a/src/Tools/8bit/fonts/isacr14.bdf	Fri Dec 13 18:25:45 1996 +0100
     8.2 +++ b/src/Tools/8bit/fonts/isacr14.bdf	Fri Dec 13 18:32:07 1996 +0100
     8.3 @@ -33,8 +33,8 @@
     8.4  FONTBOUNDINGBOX 9 14 4 -3
     8.5  STARTPROPERTIES 22
     8.6  FONTNAME_REGISTRY ""
     8.7 -FAMILY_NAME "Isabelle"
     8.8 -FOUNDRY ""
     8.9 +FAMILY_NAME "Courier"
    8.10 +FOUNDRY "Adobe"
    8.11  WEIGHT_NAME "Medium"
    8.12  SLANT "R"
    8.13  SETWIDTH_NAME "Normal"
    8.14 @@ -45,11 +45,11 @@
    8.15  RESOLUTION_Y 75
    8.16  SPACING "M"
    8.17  AVERAGE_WIDTH 90
    8.18 -CHARSET_REGISTRY ""
    8.19 +CHARSET_REGISTRY "ISO8859"
    8.20  CHARSET_ENCODING "1"
    8.21  CHARSET_COLLECTIONS ""
    8.22  FULL_NAME "Isabelle14"
    8.23 -COPYRIGHT "Copyright (c) 1985,1987 Adobe Systems,Inc.,Portions Copyright 1988 Digital Equipment Corp., Portions Copyright 1993 TU Muenchen"
    8.24 +COPYRIGHT "Copyright (c) 1985,1987 Adobe Systems,Inc.,Portions Copyright 1988 Digital Equipment Corp., Portions Copyright 1995 TU Muenchen"
    8.25  FONT_ASCENT 11
    8.26  FONT_DESCENT 3
    8.27  CAP_HEIGHT 9
     9.1 --- a/src/Tools/8bit/isa-patches/HOL/add-HOL.cfg	Fri Dec 13 18:25:45 1996 +0100
     9.2 +++ b/src/Tools/8bit/isa-patches/HOL/add-HOL.cfg	Fri Dec 13 18:32:07 1996 +0100
     9.3 @@ -1,6 +1,6 @@
     9.4  Configuration file for adding the 8bit patches to Isabelle
     9.5  
     9.6 -STEM "/usr/stud/oheimb/isabelle/"
     9.7 +STEM "/usr/wiss/oheimb/isabelle/"
     9.8  
     9.9  ADD Tools/8bit/isa-patches/HOL/HOL1.p IN HOL/HOL.thy BETWEEN "^\(\*\s*start\s*8bit\s*1" "^\(\*\s*end\s*8bit\s*1" 
    9.10  ADD Tools/8bit/isa-patches/HOL/HOL2.p IN HOL/HOL.thy BETWEEN "^\(\*\s*start\s*8bit\s*2" "^\(\*\s*end\s*8bit\s*2" 
    10.1 --- a/src/Tools/8bit/isa-patches/HOL/clean-HOL.cfg	Fri Dec 13 18:25:45 1996 +0100
    10.2 +++ b/src/Tools/8bit/isa-patches/HOL/clean-HOL.cfg	Fri Dec 13 18:32:07 1996 +0100
    10.3 @@ -1,6 +1,6 @@
    10.4  Configuration file for cleaning the 8bit patches in Isabelle
    10.5  
    10.6 -STEM "/usr/stud/oheimb/isabelle/"
    10.7 +STEM "/usr/wiss/oheimb/isabelle/"
    10.8  
    10.9  CLEAN IN HOL/HOL.thy BETWEEN "^\(\*\s*start\s*8bit\s*1" "^\(\*\s*end\s*8bit\s*1" 
   10.10  CLEAN IN HOL/HOL.thy BETWEEN "^\(\*\s*start\s*8bit\s*2" "^\(\*\s*end\s*8bit\s*2" 
    11.1 --- a/src/Tools/8bit/isa-patches/HOL/extract-HOL.cfg	Fri Dec 13 18:25:45 1996 +0100
    11.2 +++ b/src/Tools/8bit/isa-patches/HOL/extract-HOL.cfg	Fri Dec 13 18:32:07 1996 +0100
    11.3 @@ -1,6 +1,6 @@
    11.4  Configuration file for extracting the 8bit patches from Isabelle
    11.5  
    11.6 -STEM "/usr/stud/oheimb/isabelle/"
    11.7 +STEM "/usr/wiss/oheimb/isabelle/"
    11.8  
    11.9  EXTRACT Tools/8bit/isa-patches/HOL/HOL1.p IN HOL/HOL.thy BETWEEN "^\(\*\s*start\s*8bit\s*1" "^\(\*\s*end\s*8bit\s*1" 
   11.10  EXTRACT Tools/8bit/isa-patches/HOL/HOL2.p IN HOL/HOL.thy BETWEEN "^\(\*\s*start\s*8bit\s*2" "^\(\*\s*end\s*8bit\s*2" 
    12.1 --- a/src/Tools/8bit/isa-patches/HOLCF/Up3.p	Fri Dec 13 18:25:45 1996 +0100
    12.2 +++ b/src/Tools/8bit/isa-patches/HOLCF/Up3.p	Fri Dec 13 18:32:07 1996 +0100
    12.3 @@ -1,3 +1,3 @@
    12.4  translations
    12.5 -"case l of up`x => t1" == "lift`(x.t1)`l"
    12.6 +"case l of up`x => t1" == "fup`(x.t1)`l"
    12.7  
    13.1 --- a/src/Tools/8bit/isa-patches/HOLCF/add-HOLCF.cfg	Fri Dec 13 18:25:45 1996 +0100
    13.2 +++ b/src/Tools/8bit/isa-patches/HOLCF/add-HOLCF.cfg	Fri Dec 13 18:32:07 1996 +0100
    13.3 @@ -1,6 +1,6 @@
    13.4  Configuration file for adding the 8bit patches to Isabelle
    13.5  
    13.6 -STEM "/usr/stud/oheimb/isabelle/"
    13.7 +STEM "/usr/wiss/oheimb/isabelle/"
    13.8  
    13.9  ADD Tools/8bit/isa-patches/HOLCF/Cfun1.p IN HOLCF/Cfun1.thy BETWEEN "^\(\*\s*start\s*8bit\s*1" "^\(\*\s*end\s*8bit\s*1" 
   13.10  ADD Tools/8bit/isa-patches/HOLCF/Cfun1.p2 IN HOLCF/Cfun1.thy BETWEEN "^\(\*\s*start\s*8bit\s*2" "^\(\*\s*end\s*8bit\s*2" 
    14.1 --- a/src/Tools/8bit/isa-patches/HOLCF/clean-HOLCF.cfg	Fri Dec 13 18:25:45 1996 +0100
    14.2 +++ b/src/Tools/8bit/isa-patches/HOLCF/clean-HOLCF.cfg	Fri Dec 13 18:32:07 1996 +0100
    14.3 @@ -1,6 +1,6 @@
    14.4  Configuration file for cleaning the 8bit patches in Isabelle
    14.5  
    14.6 -STEM "/usr/stud/oheimb/isabelle/"
    14.7 +STEM "/usr/wiss/oheimb/isabelle/"
    14.8  
    14.9  CLEAN IN HOLCF/Cfun1.thy BETWEEN "^\(\*\s*start\s*8bit\s*1" "^\(\*\s*end\s*8bit\s*1" 
   14.10  CLEAN IN HOLCF/Cfun1.thy BETWEEN "^\(\*\s*start\s*8bit\s*2" "^\(\*\s*end\s*8bit\s*2" 
    15.1 --- a/src/Tools/8bit/isa-patches/HOLCF/extract-HOLCF.cfg	Fri Dec 13 18:25:45 1996 +0100
    15.2 +++ b/src/Tools/8bit/isa-patches/HOLCF/extract-HOLCF.cfg	Fri Dec 13 18:32:07 1996 +0100
    15.3 @@ -1,6 +1,6 @@
    15.4  Configuration file for extracting the 8bit patches from Isabelle
    15.5  
    15.6 -STEM "/usr/stud/oheimb/isabelle/"
    15.7 +STEM "/usr/wiss/oheimb/isabelle/"
    15.8  
    15.9  EXTRACT Tools/8bit/isa-patches/HOLCF/Cfun1.p IN HOLCF/Cfun1.thy BETWEEN "^\(\*\s*start\s*8bit\s*1" "^\(\*\s*end\s*8bit\s*1" 
   15.10  EXTRACT Tools/8bit/isa-patches/HOLCF/Cfun1.p2 IN HOLCF/Cfun1.thy BETWEEN "^\(\*\s*start\s*8bit\s*2" "^\(\*\s*end\s*8bit\s*2" 
    16.1 --- a/src/Tools/8bit/xemacs/isa_xemacs	Fri Dec 13 18:25:45 1996 +0100
    16.2 +++ b/src/Tools/8bit/xemacs/isa_xemacs	Fri Dec 13 18:32:07 1996 +0100
    16.3 @@ -45,7 +45,7 @@
    16.4  
    16.5  # set font as XResource
    16.6  # needed for versions later than LEmacs 19.9 
    16.7 -echo "$PREFIX*default.attributeFont: isacr14" | xrdb -merge - >/dev/null
    16.8 +echo "$PREFIX.default.attributeFont: isacr14" | xrdb -merge - >/dev/null
    16.9  
   16.10  # pop up isabelle emacs
   16.11  $ENAME \