Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
include static rail files for old manuals, to make standard make job independent of the "rail" executable;
authorwenzelm
Sun, 01 May 2011 17:55:29 +0200
changeset 42518 57367832b81a
parent 42517 b68e1c27709a
child 42519 8ac7e96f913b
include static rail files for old manuals, to make standard make job independent of the "rail" executable;
.hgignore file | annotate | diff | comparison | revisions
doc-src/HOL/Makefile file | annotate | diff | comparison | revisions
doc-src/HOL/logics-HOL.rai file | annotate | diff | comparison | revisions
doc-src/HOL/logics-HOL.rao file | annotate | diff | comparison | revisions
doc-src/HOL/logics-HOL.tex file | annotate | diff | comparison | revisions
doc-src/ZF/Makefile file | annotate | diff | comparison | revisions
doc-src/ZF/logics-ZF.rai file | annotate | diff | comparison | revisions
doc-src/ZF/logics-ZF.rao file | annotate | diff | comparison | revisions 
--- a/.hgignore	Sun May 01 17:42:21 2011 +0200
+++ b/.hgignore	Sun May 01 17:55:29 2011 +0200
@@ -20,8 +20,6 @@
 ^doc-src/.*\.lof
 ^doc-src/.*\.log
 ^doc-src/.*\.out
-^doc-src/.*\.rai
-^doc-src/.*\.rao
 ^doc-src/.*\.toc
 
 ^src/Tools/jEdit/nbproject/private/
--- a/doc-src/HOL/Makefile	Sun May 01 17:42:21 2011 +0200
+++ b/doc-src/HOL/Makefile	Sun May 01 17:55:29 2011 +0200
@@ -15,11 +15,13 @@
 FILES = logics-HOL.tex ../Logics/syntax.tex HOL.tex \
 	 ../rail.sty ../proof.sty ../iman.sty ../extra.sty ../ttbox.sty ../manual.bib
 
+rail:
+	$(RAIL) $(NAME)
+
 dvi: $(NAME).dvi
 
 $(NAME).dvi: $(FILES) isabelle_hol.eps
 	$(LATEX) $(NAME)
-	$(RAIL) $(NAME)
 	$(BIBTEX) $(NAME)
 	$(LATEX) $(NAME)
 	$(LATEX) $(NAME)
@@ -30,7 +32,6 @@
 
 $(NAME).pdf: $(FILES) isabelle_hol.pdf
 	$(PDFLATEX) $(NAME)
-	$(RAIL) $(NAME)
 	$(BIBTEX) $(NAME)
 	$(PDFLATEX) $(NAME)
 	$(PDFLATEX) $(NAME)
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/HOL/logics-HOL.rai	Sun May 01 17:55:29 2011 +0200
@@ -0,0 +1,15 @@
+\rail@i{1}{ typedef : 'typedef' ( () | '(' name ')') type '=' set witness; \par
+type : typevarlist name ( () | '(' infix ')' ); set : string; witness : () | '(' id ')'; }
+\rail@i{2}{ datatype : 'datatype' typedecls; \par
+typedecls: ( newtype '=' (cons + '|') ) + 'and' ; newtype : typevarlist id ( () | '(' infix ')' ) ; cons : name (argtype *) ( () | ( '(' mixfix ')' ) ) ; argtype : id | tid | ('(' typevarlist id ')') ; }
+\rail@t{verblbrace}
+\rail@t{verbrbrace}
+\rail@i{3}{ codegen : ( 'code_module' | 'code_library' ) modespec ? name ? \\ ( 'file' name ) ? ( 'imports' ( name + ) ) ? \\ 'contains' ( ( name '=' term ) + | term + ); \par
+modespec : '(' ( name * ) ')'; }
+\rail@i{4}{ constscode : 'consts_code' (codespec +); \par
+codespec : const template attachment ?; \par
+typescode : 'types_code' (tycodespec +); \par
+tycodespec : name template attachment ?; \par
+const : term; \par
+template: '(' string ')'; \par
+attachment: 'attach' modespec ? verblbrace text verbrbrace; }
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/HOL/logics-HOL.rao	Sun May 01 17:55:29 2011 +0200
@@ -0,0 +1,210 @@
+% This file was generated by 'rail' from 'logics-HOL.rai'
+\rail@i {1}{ typedef : 'typedef' ( () | '(' name ')') type '=' set witness; \par
+type : typevarlist name ( () | '(' infix ')' ); set : string; witness : () | '(' id ')'; }
+\rail@o {1}{
+\rail@begin{2}{typedef}
+\rail@term{typedef}[]
+\rail@bar
+\rail@nextbar{1}
+\rail@term{(}[]
+\rail@nont{name}[]
+\rail@term{)}[]
+\rail@endbar
+\rail@nont{type}[]
+\rail@term{=}[]
+\rail@nont{set}[]
+\rail@nont{witness}[]
+\rail@end
+\rail@begin{2}{type}
+\rail@nont{typevarlist}[]
+\rail@nont{name}[]
+\rail@bar
+\rail@nextbar{1}
+\rail@term{(}[]
+\rail@nont{infix}[]
+\rail@term{)}[]
+\rail@endbar
+\rail@end
+\rail@begin{1}{set}
+\rail@nont{string}[]
+\rail@end
+\rail@begin{2}{witness}
+\rail@bar
+\rail@nextbar{1}
+\rail@term{(}[]
+\rail@nont{id}[]
+\rail@term{)}[]
+\rail@endbar
+\rail@end
+}
+\rail@i {2}{ datatype : 'datatype' typedecls; \par
+typedecls: ( newtype '=' (cons + '|') ) + 'and' ; newtype : typevarlist id ( () | '(' infix ')' ) ; cons : name (argtype *) ( () | ( '(' mixfix ')' ) ) ; argtype : id | tid | ('(' typevarlist id ')') ; }
+\rail@o {2}{
+\rail@begin{1}{datatype}
+\rail@term{datatype}[]
+\rail@nont{typedecls}[]
+\rail@end
+\rail@begin{3}{typedecls}
+\rail@plus
+\rail@nont{newtype}[]
+\rail@term{=}[]
+\rail@plus
+\rail@nont{cons}[]
+\rail@nextplus{1}
+\rail@cterm{|}[]
+\rail@endplus
+\rail@nextplus{2}
+\rail@cterm{and}[]
+\rail@endplus
+\rail@end
+\rail@begin{2}{newtype}
+\rail@nont{typevarlist}[]
+\rail@nont{id}[]
+\rail@bar
+\rail@nextbar{1}
+\rail@term{(}[]
+\rail@nont{infix}[]
+\rail@term{)}[]
+\rail@endbar
+\rail@end
+\rail@begin{2}{cons}
+\rail@nont{name}[]
+\rail@plus
+\rail@nextplus{1}
+\rail@cnont{argtype}[]
+\rail@endplus
+\rail@bar
+\rail@nextbar{1}
+\rail@term{(}[]
+\rail@nont{mixfix}[]
+\rail@term{)}[]
+\rail@endbar
+\rail@end
+\rail@begin{3}{argtype}
+\rail@bar
+\rail@nont{id}[]
+\rail@nextbar{1}
+\rail@nont{tid}[]
+\rail@nextbar{2}
+\rail@term{(}[]
+\rail@nont{typevarlist}[]
+\rail@nont{id}[]
+\rail@term{)}[]
+\rail@endbar
+\rail@end
+}
+\rail@t {verblbrace}
+\rail@t {verbrbrace}
+\rail@i {3}{ codegen : ( 'code_module' | 'code_library' ) modespec ? name ? \\ ( 'file' name ) ? ( 'imports' ( name + ) ) ? \\ 'contains' ( ( name '=' term ) + | term + ); \par
+modespec : '(' ( name * ) ')'; }
+\rail@o {3}{
+\rail@begin{11}{codegen}
+\rail@bar
+\rail@term{code_module}[]
+\rail@nextbar{1}
+\rail@term{code_library}[]
+\rail@endbar
+\rail@bar
+\rail@nextbar{1}
+\rail@nont{modespec}[]
+\rail@endbar
+\rail@bar
+\rail@nextbar{1}
+\rail@nont{name}[]
+\rail@endbar
+\rail@cr{3}
+\rail@bar
+\rail@nextbar{4}
+\rail@term{file}[]
+\rail@nont{name}[]
+\rail@endbar
+\rail@bar
+\rail@nextbar{4}
+\rail@term{imports}[]
+\rail@plus
+\rail@nont{name}[]
+\rail@nextplus{5}
+\rail@endplus
+\rail@endbar
+\rail@cr{7}
+\rail@term{contains}[]
+\rail@bar
+\rail@plus
+\rail@nont{name}[]
+\rail@term{=}[]
+\rail@nont{term}[]
+\rail@nextplus{8}
+\rail@endplus
+\rail@nextbar{9}
+\rail@plus
+\rail@nont{term}[]
+\rail@nextplus{10}
+\rail@endplus
+\rail@endbar
+\rail@end
+\rail@begin{2}{modespec}
+\rail@term{(}[]
+\rail@plus
+\rail@nextplus{1}
+\rail@cnont{name}[]
+\rail@endplus
+\rail@term{)}[]
+\rail@end
+}
+\rail@i {4}{ constscode : 'consts_code' (codespec +); \par
+codespec : const template attachment ?; \par
+typescode : 'types_code' (tycodespec +); \par
+tycodespec : name template attachment ?; \par
+const : term; \par
+template: '(' string ')'; \par
+attachment: 'attach' modespec ? verblbrace text verbrbrace; }
+\rail@o {4}{
+\rail@begin{2}{constscode}
+\rail@term{consts_code}[]
+\rail@plus
+\rail@nont{codespec}[]
+\rail@nextplus{1}
+\rail@endplus
+\rail@end
+\rail@begin{2}{codespec}
+\rail@nont{const}[]
+\rail@nont{template}[]
+\rail@bar
+\rail@nextbar{1}
+\rail@nont{attachment}[]
+\rail@endbar
+\rail@end
+\rail@begin{2}{typescode}
+\rail@term{types_code}[]
+\rail@plus
+\rail@nont{tycodespec}[]
+\rail@nextplus{1}
+\rail@endplus
+\rail@end
+\rail@begin{2}{tycodespec}
+\rail@nont{name}[]
+\rail@nont{template}[]
+\rail@bar
+\rail@nextbar{1}
+\rail@nont{attachment}[]
+\rail@endbar
+\rail@end
+\rail@begin{1}{const}
+\rail@nont{term}[]
+\rail@end
+\rail@begin{1}{template}
+\rail@term{(}[]
+\rail@nont{string}[]
+\rail@term{)}[]
+\rail@end
+\rail@begin{2}{attachment}
+\rail@term{attach}[]
+\rail@bar
+\rail@nextbar{1}
+\rail@nont{modespec}[]
+\rail@endbar
+\rail@token{verblbrace}[]
+\rail@nont{text}[]
+\rail@token{verbrbrace}[]
+\rail@end
+}
--- a/doc-src/HOL/logics-HOL.tex	Sun May 01 17:42:21 2011 +0200
+++ b/doc-src/HOL/logics-HOL.tex	Sun May 01 17:55:29 2011 +0200
@@ -1,5 +1,6 @@
 %% $Id$
 \documentclass[12pt,a4paper]{report}
+\usepackage{../../lib/texinputs/isabelle,../../lib/texinputs/isabellesym}
 \usepackage{graphicx,../iman,../extra,../ttbox,../proof,../rail,../railsetup,latexsym,../pdfsetup}
 
 %%% to index derived rls:  ^\([a-zA-Z0-9][a-zA-Z0-9_]*\)        \\tdx{\1}  
--- a/doc-src/ZF/Makefile	Sun May 01 17:42:21 2011 +0200
+++ b/doc-src/ZF/Makefile	Sun May 01 17:55:29 2011 +0200
@@ -16,11 +16,13 @@
   ../rail.sty ../proof.sty ../iman.sty ../extra.sty ../ttbox.sty	\
   ../../lib/texinputs/isabelle.sty ../../lib/texinputs/isabellesym.sty ../pdfsetup.sty ../manual.bib
 
+rail:
+	$(RAIL) $(NAME)
+
 dvi: $(NAME).dvi
 
 $(NAME).dvi: $(FILES) isabelle_zf.eps
 	$(LATEX) $(NAME)
-	$(RAIL) $(NAME)
 	$(BIBTEX) $(NAME)
 	$(LATEX) $(NAME)
 	$(LATEX) $(NAME)
@@ -31,7 +33,6 @@
 
 $(NAME).pdf: $(FILES) isabelle_zf.pdf
 	$(PDFLATEX) $(NAME)
-	$(RAIL) $(NAME)
 	$(BIBTEX) $(NAME)
 	$(PDFLATEX) $(NAME)
 	$(PDFLATEX) $(NAME)
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/ZF/logics-ZF.rai	Sun May 01 17:55:29 2011 +0200
@@ -0,0 +1,2 @@
+\rail@i{1}{ datatype : ( 'datatype' | 'codatatype' ) datadecls; \par
+datadecls: ( '"' id arglist '"' '=' (constructor + '|') ) + 'and' ; constructor : name ( () | consargs ) ( () | ( '(' mixfix ')' ) ) ; consargs : '(' ('"' var ' : ' term '"' + ',') ')' ; }
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/ZF/logics-ZF.rao	Sun May 01 17:55:29 2011 +0200
@@ -0,0 +1,55 @@
+% This file was generated by 'rail' from 'logics-ZF.rai'
+\rail@i {1}{ datatype : ( 'datatype' | 'codatatype' ) datadecls; \par
+datadecls: ( '"' id arglist '"' '=' (constructor + '|') ) + 'and' ; constructor : name ( () | consargs ) ( () | ( '(' mixfix ')' ) ) ; consargs : '(' ('"' var ' : ' term '"' + ',') ')' ; }
+\rail@o {1}{
+\rail@begin{2}{datatype}
+\rail@bar
+\rail@term{datatype}[]
+\rail@nextbar{1}
+\rail@term{codatatype}[]
+\rail@endbar
+\rail@nont{datadecls}[]
+\rail@end
+\rail@begin{3}{datadecls}
+\rail@plus
+\rail@term{"}[]
+\rail@nont{id}[]
+\rail@nont{arglist}[]
+\rail@term{"}[]
+\rail@term{=}[]
+\rail@plus
+\rail@nont{constructor}[]
+\rail@nextplus{1}
+\rail@cterm{|}[]
+\rail@endplus
+\rail@nextplus{2}
+\rail@cterm{and}[]
+\rail@endplus
+\rail@end
+\rail@begin{2}{constructor}
+\rail@nont{name}[]
+\rail@bar
+\rail@nextbar{1}
+\rail@nont{consargs}[]
+\rail@endbar
+\rail@bar
+\rail@nextbar{1}
+\rail@term{(}[]
+\rail@nont{mixfix}[]
+\rail@term{)}[]
+\rail@endbar
+\rail@end
+\rail@begin{2}{consargs}
+\rail@term{(}[]
+\rail@plus
+\rail@term{"}[]
+\rail@nont{var}[]
+\rail@term{ : }[]
+\rail@nont{term}[]
+\rail@term{"}[]
+\rail@nextplus{1}
+\rail@cterm{,}[]
+\rail@endplus
+\rail@term{)}[]
+\rail@end
+}
isabelle