Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
doc-src/TutorialI/isa-index
author hoelzl
Mon, 23 Aug 2010 19:35:57 +0200
changeset 38656 d5d342611edb
parent 11404 280436a346ca
permissions -rwxr-xr-x
Rewrite the Probability theory. Introduced pinfreal as real numbers with infinity. Use pinfreal as value for measures. Introduces Lebesgue Measure based on the integral in Multivariate Analysis. Proved Radon Nikodym for arbitrary sigma finite measure spaces.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
11400
ddcfdc38090d isa-index replaces ../sedindex: knows about \\isa
paulson
parents:
diff changeset 
     1
 
#! /bin/sh
ddcfdc38090d isa-index replaces ../sedindex: knows about \\isa
paulson
parents:
diff changeset 
     2
 
#
ddcfdc38090d isa-index replaces ../sedindex: knows about \\isa
paulson
parents:
diff changeset 
     3
 
#sedindex - shell script to create indexes, preprocessing LaTeX's .idx file
ddcfdc38090d isa-index replaces ../sedindex: knows about \\isa
paulson
parents:
diff changeset 
     4
 
#
ddcfdc38090d isa-index replaces ../sedindex: knows about \\isa
paulson
parents:
diff changeset 
     5
 
#  puts strings prefixed by * into \tt font
ddcfdc38090d isa-index replaces ../sedindex: knows about \\isa
paulson
parents:
diff changeset 
     6
 
#    terminator characters for strings are |!@{}
ddcfdc38090d isa-index replaces ../sedindex: knows about \\isa
paulson
parents:
diff changeset 
     7
 
#
ddcfdc38090d isa-index replaces ../sedindex: knows about \\isa
paulson
parents:
diff changeset 
     8
 
# a space terminates the \tt part to allow \index{*notE theorem}, etc.
ddcfdc38090d isa-index replaces ../sedindex: knows about \\isa
paulson
parents:
diff changeset 
     9
 
#
ddcfdc38090d isa-index replaces ../sedindex: knows about \\isa
paulson
parents:
diff changeset 
    10
 
# note that makeindex uses a dboule quote (") to delimit special characters.
ddcfdc38090d isa-index replaces ../sedindex: knows about \\isa
paulson
parents:
diff changeset 
    11
 
#
ddcfdc38090d isa-index replaces ../sedindex: knows about \\isa
paulson
parents:
diff changeset 
    12
 
# change *"X"Y"Z"W  to  "X"Y"Z"W@{\tt "X"Y"Z"W}
ddcfdc38090d isa-index replaces ../sedindex: knows about \\isa
paulson
parents:
diff changeset 
    13
 
# change *"X"Y"Z    to  "X"Y"Z@{\tt "X"Y"Z}
ddcfdc38090d isa-index replaces ../sedindex: knows about \\isa
paulson
parents:
diff changeset 
    14
 
# change *"X"Y      to  "X"Y@{\tt "X"Y}
ddcfdc38090d isa-index replaces ../sedindex: knows about \\isa
paulson
parents:
diff changeset 
    15
 
# change *"X        to  "X@{\tt "X}
ddcfdc38090d isa-index replaces ../sedindex: knows about \\isa
paulson
parents:
diff changeset 
    16
 
# change *IDENT  to  IDENT@{\tt IDENT}
ddcfdc38090d isa-index replaces ../sedindex: knows about \\isa
paulson
parents:
diff changeset 
    17
 
#    where IDENT is any string not containing | ! or @
ddcfdc38090d isa-index replaces ../sedindex: knows about \\isa
paulson
parents:
diff changeset 
    18
 
# FOUR backslashes: to escape the shell AND sed
11404
280436a346ca careful changes to make its output identical to that of indexing macros
paulson
parents: 11400
diff changeset 
    19
 
sed -e "s~\*\(\".\".\".\".\)~\1@\\\\isa {\1}~g
280436a346ca careful changes to make its output identical to that of indexing macros
paulson
parents: 11400
diff changeset 
    20
 
s~\*\(\".\".\".\)~\1@\\\\isa {\1}~g
280436a346ca careful changes to make its output identical to that of indexing macros
paulson
parents: 11400
diff changeset 
    21
 
s~\*\(\".\".\)~\1@\\\\isa {\1}~g
280436a346ca careful changes to make its output identical to that of indexing macros
paulson
parents: 11400
diff changeset 
    22
 
s~\*\(\".\)~\1@\\\\isa {\1}~g
280436a346ca careful changes to make its output identical to that of indexing macros
paulson
parents: 11400
diff changeset 
    23
 
s~\*\([^ |!@{}][^ |!@{}]*\)~\1@\\\\isa {\1}~g" $1.idx | makeindex -c -q -o $1.ind
isabelle