# HG changeset patch
# User wenzelm
# Date 1379772497 -7200
# Node ID 17e93676670b7f091df81326866832e35d79fa0e
# Parent  db362319d7665250a51d870073fe267274585ff7
tuned;

diff -r db362319d766 -r 17e93676670b src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Sat Sep 21 15:23:31 2013 +0200
+++ b/src/Doc/JEdit/JEdit.thy	Sat Sep 21 16:08:17 2013 +0200
@@ -45,7 +45,7 @@
   \begin{itemize}
 
   \item The original jEdit look-and-feel is generally preserved, although
-  some default properties have been changed to accommodate Isabelle (e.g.
+  some default properties have been changed to accommodate Isabelle (e.g.\
   the text area font).
 
   \item Formal Isabelle/Isar text is checked asynchronously while editing.
@@ -112,28 +112,28 @@
   \item use the \emph{Symbols} dockable window
   \item copy/paste from decoded source files
   \item copy/paste from prover output
-  \item completion provided by Isabelle plugin, e.g.
+  \item completion provided by Isabelle plugin, e.g.\
 
   \medskip
   \begin{tabular}{lll}
-    \textbf{backslash escape} & \textbf{abbreviation} & \textbf{symbol} \\[1ex]
+    \textbf{symbol} & \textbf{abbreviation} & \textbf{backslash escape} \\[1ex]
 
-    @{verbatim "\\lambda"}         & @{verbatim "%"}     & @{text "\<lambda>"} \\
-    @{verbatim "\\Rightarrow"}     & @{verbatim "=>"}    & @{text "\<Rightarrow>"} \\
-    @{verbatim "\\Longrightarrow"} & @{verbatim "==>"}   & @{text "\<Longrightarrow>"} \\
+    @{text "\<lambda>"}   & @{verbatim "%"}     &  @{verbatim "\\lambda"}         \\
+    @{text "\<Rightarrow>"}  & @{verbatim "=>"}    &  @{verbatim "\\Rightarrow"}     \\
+    @{text "\<Longrightarrow>"} & @{verbatim "==>"}   &  @{verbatim "\\Longrightarrow"} \\
 
-    @{verbatim "\\And"}            & @{verbatim "!!"}    & @{text "\<And>"} \\
-    @{verbatim "\\equiv"}          & @{verbatim "=="}    & @{text "\<equiv>"} \\
+    @{text "\<And>"}  & @{verbatim "!!"}    &  @{verbatim "\\And"}            \\
+    @{text "\<equiv>"}  & @{verbatim "=="}    &  @{verbatim "\\equiv"}          \\
 
-    @{verbatim "\\forall"}         & @{verbatim "!"}     & @{text "\<forall>"} \\
-    @{verbatim "\\exists"}         & @{verbatim "?"}     & @{text "\<exists>"} \\
-    @{verbatim "\\longrightarrow"} & @{verbatim "-->"}   & @{text "\<longrightarrow>"} \\
-    @{verbatim "\\and"}            & @{verbatim "&"}     & @{text "\<and>"} \\
-    @{verbatim "\\or"}             & @{verbatim "|"}     & @{text "\<or>"} \\
-    @{verbatim "\\not"}            & @{verbatim "~"}     & @{text "\<not>"} \\
-    @{verbatim "\\noteq"}          & @{verbatim "~="}    & @{text "\<noteq>"} \\
-    @{verbatim "\\in"}             & @{verbatim ":"}     & @{text "\<in>"} \\
-    @{verbatim "\\notin"}          & @{verbatim "~:"}    & @{text "\<notin>"} \\
+    @{text "\<forall>"}   & @{verbatim "!"}     &  @{verbatim "\\forall"}         \\
+    @{text "\<exists>"}   & @{verbatim "?"}     &  @{verbatim "\\exists"}         \\
+    @{text "\<longrightarrow>"} & @{verbatim "-->"}   &  @{verbatim "\\longrightarrow"} \\
+    @{text "\<and>"}   & @{verbatim "&"}     &  @{verbatim "\\and"}            \\
+    @{text "\<or>"}   & @{verbatim "|"}     &  @{verbatim "\\or"}             \\
+    @{text "\<not>"}   & @{verbatim "~"}     &  @{verbatim "\\not"}            \\
+    @{text "\<noteq>"}   & @{verbatim "~="}    &  @{verbatim "\\noteq"}          \\
+    @{text "\<in>"}   & @{verbatim ":"}     &  @{verbatim "\\in"}             \\
+    @{text "\<notin>"}   & @{verbatim "~:"}    &  @{verbatim "\\notin"}          \\
   \end{tabular}
 
   \end{enumerate}
@@ -150,7 +150,7 @@
   sequences coincide with the symbol mapping.
 
   \item Raw Unicode characters within prover source files should be
-  restricted to informal parts, e.g. to write text in non-latin alphabets.
+  restricted to informal parts, e.g.\ to write text in non-latin alphabets.
   Mathematical symbols should be defined via the official rendering tables.
 
   \end{itemize}
@@ -189,7 +189,7 @@
   jEdit Shortcuts options dialog.
 
   \item \textbf{Problem:} Lack of dependency management for auxiliary files
-  that contribute to a theory (e.g. @{command ML_file}).
+  that contribute to a theory (e.g.\ @{command ML_file}).
 
   \textbf{Workaround:} Re-load files manually within the prover.
 
diff -r db362319d766 -r 17e93676670b src/Doc/JEdit/document/root.tex
--- a/src/Doc/JEdit/document/root.tex	Sat Sep 21 15:23:31 2013 +0200
+++ b/src/Doc/JEdit/document/root.tex	Sat Sep 21 16:08:17 2013 +0200
@@ -30,8 +30,9 @@
 \subsubsection*{Acknowledgements}
 
 Research and implementation of concepts around PIDE and Isabelle/jEdit has
-started around 2008 and was kindly supported by
+started around 2008 and was kindly supported by:
 \begin{itemize}
+\item TU M\"unchen \url{http://in.tum.de}
 \item BMBF \url{http://www.bmbf.de}
 \item Universit\'e Paris-Sud \url{http://www.u-psud.fr}
 \item Digiteo \url{http://www.digiteo.fr}