# HG changeset patch
# User haftmann
# Date 1117914235 -7200
# Node ID 95cc0e8f8a17c7555ee3f667ceb7fc8e7f7d4534
# Parent 5be516f79075bbd58c85a0de91a38accacf73723
added shellcmd style
diff -r 5be516f79075 -r 95cc0e8f8a17 Admin/website/build/pypager.py
--- a/Admin/website/build/pypager.py Sat Jun 04 21:42:50 2005 +0200
+++ b/Admin/website/build/pypager.py Sat Jun 04 21:43:55 2005 +0200
@@ -122,10 +122,6 @@
handler.characters(u"%i%sKB" % (size / 1024, unichr(160)))
handler.endElement(u"td")
- def cvs(self, handler, **args):
-
- pass
-
# a notion of paths
class PathCalculator:
@@ -354,6 +350,8 @@
def processingInstruction(self, target, data):
+ print '*', target
+ print '*', data
self.closeLastStart()
self.flushCharacterBuffer()
func = getattr(self._func, target)
diff -r 5be516f79075 -r 95cc0e8f8a17 Admin/website/community.html
--- a/Admin/website/community.html Sat Jun 04 21:42:50 2005 +0200
+++ b/Admin/website/community.html Sat Jun 04 21:43:55 2005 +0200
@@ -1,6 +1,6 @@
-
+
diff -r 5be516f79075 -r 95cc0e8f8a17 Admin/website/dist/css/isabelle_base.css
--- a/Admin/website/dist/css/isabelle_base.css Sat Jun 04 21:42:50 2005 +0200
+++ b/Admin/website/dist/css/isabelle_base.css Sat Jun 04 21:43:55 2005 +0200
@@ -146,13 +146,13 @@
margin-top: 1ex;
margin-bottom: 1ex;
margin-left: 4em;
+ margin-right: 4em;
padding-left: 0pt;
}
ul.shellcmd li:before {
content: "$ ";
font-weight: bold;
- font-size: 40pt;
}
/* the faq */
diff -r 5be516f79075 -r 95cc0e8f8a17 Admin/website/faq.html
--- a/Admin/website/faq.html Sat Jun 04 21:42:50 2005 +0200
+++ b/Admin/website/faq.html Sat Jun 04 21:43:55 2005 +0200
@@ -1,6 +1,6 @@
-
+
@@ -182,17 +182,22 @@
in strange ways. One solution is to run the Emacs process itself with an
altered locale setting, for example, starting XEmacs by typing:
- $ LC_CTYPE=en_GB Isabelle &
+
+ - LC_CTYPE=en_GB Isabelle &
+
The supplied proofgeneral script makes this setting if it sees the string
- UTF in the current value of LC_CTYPE. Depending on your distribution, this
- variable might also be called LANG.
+ UTF in the current value of LC_CTYPE.
+ Depending on your distribution, this
+ variable might also be called LANG.
- Alternatively you can set LC_CTYPE or LANG inside a file ~/.i18n, which
- will be read by the shell. This will affect all applications, though. [
- suggestions for a better workaround inside Emacs would be welcome ]
+ Alternatively you can set LC_CTYPE or
+ LANG inside a file ~/.i18n, which
+ will be read by the shell. This will affect all applications, though.
+
+
Suggestions for a better workaround inside Emacs would be welcomed;
- NB: a related issue is warnings from x-symbol: "Emacs language environment
+
A related issue is warnings from x-symbol: "Emacs language environment
and system locale specify different encoding, I'll assume `iso-8859-1'". This
warning appears to be mainly harmless. Notice that the variable
`buffer-file-coding-system' may determine the format that files are saved
@@ -231,14 +236,14 @@
I want to generate one of those flashy LaTeX documents. How?
- You will need to work with the isatool command for this (in
+ You will need to work with the isatool command for this (in
a Unix shell). The easiest way to get to a document is the following: use
- isatool mkdir to set up a new directory. The command will also
- create a file called IsaMakefile in the current directory. Put
+ isatool mkdir to set up a new directory. The command will also
+ create a file called IsaMakefile in the current directory. Put
your theory file(s) into the new directory and edit the file
- ROOT.ML in there (following the comments) to tell Isabelle which
+ ROOT.ML in there (following the comments) to tell Isabelle which
of the theories to load (and in which order). Go back to the parent
- directory (where the IsaMakefile is) and type isatool
+ directory (where the IsaMakefile is) and type isatool
make. Isabelle should then process your theories and tell you where
to find the finished document. For more information on generating
documents see the Isabelle Tutorial, Chapter 4.
@@ -248,10 +253,10 @@
No, you can tell Isabelle to build a so-called heap image. This heap
image can contain your preloaded theories. To get one, set up a directory
- with a ROOT.ML file (as for generating a document) and use the
- command isatool usedir -b HOL MyImage in that directory to
- create an image MyImage using the parent logic HOL. You
- should then be able to invoke Isabelle with Isabelle -l MyImage
+ with a ROOT.ML file (as for generating a document) and use the
+ command isatool usedir -b HOL MyImage in that directory to
+ create an image MyImage using the parent logic HOL. You
+ should then be able to invoke Isabelle with Isabelle -l MyImage
and have everything that is loaded in ROOT.ML instantly available.
Does Isabelle run on Windows?
diff -r 5be516f79075 -r 95cc0e8f8a17 Admin/website/index.html
--- a/Admin/website/index.html Sat Jun 04 21:42:50 2005 +0200
+++ b/Admin/website/index.html Sat Jun 04 21:43:55 2005 +0200
@@ -1,6 +1,6 @@
-
+
diff -r 5be516f79075 -r 95cc0e8f8a17 Admin/website/logics.html
--- a/Admin/website/logics.html Sat Jun 04 21:42:50 2005 +0200
+++ b/Admin/website/logics.html Sat Jun 04 21:43:55 2005 +0200
@@ -1,6 +1,6 @@
-
+
diff -r 5be516f79075 -r 95cc0e8f8a17 Admin/website/overview.html
--- a/Admin/website/overview.html Sat Jun 04 21:42:50 2005 +0200
+++ b/Admin/website/overview.html Sat Jun 04 21:43:55 2005 +0200
@@ -1,6 +1,6 @@
-
+
@@ -73,7 +73,7 @@
Isabelle is closely integrated with the ProofGeneral user interface, which
eases the task of writing and maintaining proof scripts.
-
+
Preview