--- a/doc-src/IsarRef/isar-ref.tex Fri Dec 03 14:00:55 2010 +0100
+++ b/doc-src/IsarRef/isar-ref.tex Fri Dec 03 17:18:41 2010 +0100
@@ -1,7 +1,6 @@
\documentclass[12pt,a4paper,fleqn]{report}
\usepackage{amssymb}
\usepackage[greek,english]{babel}
-\usepackage[latin1]{inputenc}
\usepackage[only,bigsqcap]{stmaryrd}
\usepackage{textcomp}
\usepackage{latexsym}
--- a/doc-src/isabellesym.sty Fri Dec 03 14:00:55 2010 +0100
+++ b/doc-src/isabellesym.sty Fri Dec 03 17:18:41 2010 +0100
@@ -324,12 +324,12 @@
\newcommand{\isasymregistered}{\isatext{\rm\textregistered}}
\newcommand{\isasymhyphen}{\isatext{\rm-}}
\newcommand{\isasyminverse}{\isamath{{}^{-1}}}
-\newcommand{\isasymonesuperior}{\isamath{\mathonesuperior}} %requires latin1
-\newcommand{\isasymonequarter}{\isatext{\rm\textonequarter}} %requires latin1
-\newcommand{\isasymtwosuperior}{\isamath{\mathtwosuperior}} %requires latin1
-\newcommand{\isasymonehalf}{\isatext{\rm\textonehalf}} %requires latin1
-\newcommand{\isasymthreesuperior}{\isamath{\maththreesuperior}} %requires latin1
-\newcommand{\isasymthreequarters}{\isatext{\rm\textthreequarters}} %requires latin1
+\newcommand{\isasymonesuperior}{\isamath{{}^1}}
+\newcommand{\isasymonequarter}{\isatext{\rm\textonequarter}} %requires textcomp
+\newcommand{\isasymtwosuperior}{\isamath{{}^2}}
+\newcommand{\isasymonehalf}{\isatext{\rm\textonehalf}} %requires textcomp
+\newcommand{\isasymthreesuperior}{\isamath{{}^3}}
+\newcommand{\isasymthreequarters}{\isatext{\rm\textthreequarters}} %requires textcomp
\newcommand{\isasymordfeminine}{\isatext{\rm\textordfeminine}}
\newcommand{\isasymordmasculine}{\isatext{\rm\textordmasculine}}
\newcommand{\isasymsection}{\isatext{\rm\S}}
@@ -341,7 +341,7 @@
\newcommand{\isasymyen}{\isatext{\yen}} %requires amssymb
\newcommand{\isasymcent}{\isatext{\textcent}} %requires textcomp
\newcommand{\isasymcurrency}{\isatext{\textcurrency}} %requires textcomp
-\newcommand{\isasymdegree}{\isatext{\rm\textdegree}} %requires latin1
+\newcommand{\isasymdegree}{\isatext{\rm\textdegree}} %requires textcomp
\newcommand{\isasymamalg}{\isamath{\amalg}}
\newcommand{\isasymmho}{\isamath{\mho}} %requires amssymb
\newcommand{\isasymlozenge}{\isamath{\lozenge}} %requires amssymb
--- a/lib/Tools/latex Fri Dec 03 14:00:55 2010 +0100
+++ b/lib/Tools/latex Fri Dec 03 17:18:41 2010 +0100
@@ -88,7 +88,7 @@
function extract_syms ()
{
perl -n \
- -e '(!m,%requires, || m,%requires latin1, || m,%requires amssymb, || m,%requires textcomp,) && m,\\newcommand\{\\isasym(\w+)\}, && print "$1\n";' \
+ -e '(!m,%requires, || m,%requires amssymb, || m,%requires textcomp,) && m,\\newcommand\{\\isasym(\w+)\}, && print "$1\n";' \
"$ISABELLE_HOME/lib/texinputs/isabellesym.sty" > "$DIR/syms.lst"
perl -n \
-e 'm,\\newcommand\{\\isactrl(\w+)\}, && print "$1\n";' \
--- a/lib/Tools/mkdir Fri Dec 03 14:00:55 2010 +0100
+++ b/lib/Tools/mkdir Fri Dec 03 17:18:41 2010 +0100
@@ -221,10 +221,6 @@
%option greek for \<euro>
%option english (default language) for \<guillemotleft>, \<guillemotright>
-%\usepackage[latin1]{inputenc}
- %for \<onesuperior>, \<onequarter>, \<twosuperior>, \<onehalf>,
- %\<threesuperior>, \<threequarters>, \<degree>
-
%\usepackage[only,bigsqcap]{stmaryrd}
%for \<Sqinter>
@@ -232,7 +228,8 @@
%for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
%\usepackage{textcomp}
- %for \<cent>, \<currency>
+ %for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,
+ %\<currency>
% this should be the last package used
\usepackage{pdfsetup}
--- a/lib/texinputs/draft.tex Fri Dec 03 14:00:55 2010 +0100
+++ b/lib/texinputs/draft.tex Fri Dec 03 17:18:41 2010 +0100
@@ -6,7 +6,6 @@
\usepackage{isabelle,isabellesym,pdfsetup}
%packages for unusual symbols according to 'isabelle latex -o syms'
-\usepackage[latin1]{inputenc}
\usepackage{amssymb}
\usepackage{textcomp}
--- a/lib/texinputs/isabellesym.sty Fri Dec 03 14:00:55 2010 +0100
+++ b/lib/texinputs/isabellesym.sty Fri Dec 03 17:18:41 2010 +0100
@@ -324,12 +324,12 @@
\newcommand{\isasymregistered}{\isatext{\rm\textregistered}}
\newcommand{\isasymhyphen}{\isatext{\rm-}}
\newcommand{\isasyminverse}{\isamath{{}^{-1}}}
-\newcommand{\isasymonesuperior}{\isamath{\mathonesuperior}} %requires latin1
-\newcommand{\isasymonequarter}{\isatext{\rm\textonequarter}} %requires latin1
-\newcommand{\isasymtwosuperior}{\isamath{\mathtwosuperior}} %requires latin1
-\newcommand{\isasymonehalf}{\isatext{\rm\textonehalf}} %requires latin1
-\newcommand{\isasymthreesuperior}{\isamath{\maththreesuperior}} %requires latin1
-\newcommand{\isasymthreequarters}{\isatext{\rm\textthreequarters}} %requires latin1
+\newcommand{\isasymonesuperior}{\isamath{{}^1}}
+\newcommand{\isasymonequarter}{\isatext{\rm\textonequarter}} %requires textcomp
+\newcommand{\isasymtwosuperior}{\isamath{{}^2}}
+\newcommand{\isasymonehalf}{\isatext{\rm\textonehalf}} %requires textcomp
+\newcommand{\isasymthreesuperior}{\isamath{{}^3}}
+\newcommand{\isasymthreequarters}{\isatext{\rm\textthreequarters}} %requires textcomp
\newcommand{\isasymordfeminine}{\isatext{\rm\textordfeminine}}
\newcommand{\isasymordmasculine}{\isatext{\rm\textordmasculine}}
\newcommand{\isasymsection}{\isatext{\rm\S}}
@@ -341,7 +341,7 @@
\newcommand{\isasymyen}{\isatext{\yen}} %requires amssymb
\newcommand{\isasymcent}{\isatext{\textcent}} %requires textcomp
\newcommand{\isasymcurrency}{\isatext{\textcurrency}} %requires textcomp
-\newcommand{\isasymdegree}{\isatext{\rm\textdegree}} %requires latin1
+\newcommand{\isasymdegree}{\isatext{\rm\textdegree}} %requires textcomp
\newcommand{\isasymamalg}{\isamath{\amalg}}
\newcommand{\isasymmho}{\isamath{\mho}} %requires amssymb
\newcommand{\isasymlozenge}{\isamath{\lozenge}} %requires amssymb
--- a/src/Pure/Concurrent/bash.ML Fri Dec 03 14:00:55 2010 +0100
+++ b/src/Pure/Concurrent/bash.ML Fri Dec 03 17:18:41 2010 +0100
@@ -64,8 +64,7 @@
in () end;
fun cleanup () =
- (terminate ();
- Simple_Thread.interrupt system_thread;
+ (Simple_Thread.interrupt system_thread;
try File.rm script_path;
try File.rm output_path;
try File.rm pid_path);
@@ -79,6 +78,6 @@
val rc = (case Synchronized.value result of Signal => Exn.interrupt () | Result rc => rc);
val _ = cleanup ();
in (output, rc) end
- handle exn => (cleanup (); reraise exn)
+ handle exn => (terminate(); cleanup (); reraise exn)
end);
--- a/src/Tools/jEdit/dist-template/README.html Fri Dec 03 14:00:55 2010 +0100
+++ b/src/Tools/jEdit/dist-template/README.html Fri Dec 03 17:18:41 2010 +0100
@@ -15,7 +15,7 @@
<li>The original jEdit look-and-feel is generally preserved, although
some default properties have been changed to accommodate Isabelle
- (e.g. main the text area font).</li>
+ (e.g. the text area font).</li>
<li>Formal Isabelle/Isar text is checked asynchronously while editing.
The user is in full command of the editor, and the prover refrains