diff -r f6a001b47a84 -r 6548da70f14e doc-src/isac/msteger/bakk-presentation.tex --- a/doc-src/isac/msteger/bakk-presentation.tex Sat Jun 18 11:28:10 2011 +0200 +++ b/doc-src/isac/msteger/bakk-presentation.tex Mon Jun 20 17:33:06 2011 +0200 @@ -124,57 +124,21 @@ \end{frame} \subsection[Integration]{Isabelles Filestruktur im \"Ubergangsstadium} -\begin{frame}\frametitle{Isabelle Files: *.jar} -{\footnotesize ------ for ``isabelle jedit \&''; contained in Isabelle\_bundle}\\ -{\tiny -./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jedit.jar\\ -./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/LatestVersion.jar\\ -./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/SideKick.jar\\ -./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/Console.jar\\ -./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/Pure.jar \alert{$\;\;\;\;\;\;\;\;\;\;\;\Longleftarrow$ entry to SML}\\ -./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/Isac.jar\\ -./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/scala-compiler.jar\\ -./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/Isabelle-jEdit.jar\\ -./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/cobra.jar\\ -./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/js.jar\\ -./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/Hyperlinks.jar\\ -./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/scala-swing.jar\\ -./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/scala-library.jar\\ -./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/QuickNotepad.jar\\ -./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/ErrorList.jar\\ - -{\footnotesize ------ scala system; contained in Isabelle\_bundle}\\ -./contrib/scala-2.8.1.final/misc/sbaz/scala-bazaars.jar\\ -./contrib/scala-2.8.1.final/misc/sbaz/sbaz-tests.jar\\ -./contrib/scala-2.8.1.final/misc/scala-devel/plugins/continuations.jar\\ -./contrib/scala-2.8.1.final/lib/scala-compiler.jar\\ -./contrib/scala-2.8.1.final/lib/scalap.jar\\ -./contrib/scala-2.8.1.final/lib/scala-swing.jar\\ -./contrib/scala-2.8.1.final/lib/scala-library.jar\\ -./contrib/scala-2.8.1.final/lib/jline.jar\\ -./contrib/scala-2.8.1.final/lib/scala-dbc.jar\\ -./contrib/scala-2.8.1.final/src/scala-library-src.jar\\ -./contrib/scala-2.8.1.final/src/scala-swing-src.jar\\ -./contrib/scala-2.8.1.final/src/scala-compiler-src.jar\\ -./contrib/scala-2.8.1.final/src/scala-dbc-src.jar\\ -./contrib/scala-2.8.1.final/src/sbaz-src.jar\\ -} -\end{frame} \begin{frame}\frametitle{Isabelle Files: *.scala} {\tiny +\textbf{\$ find -name ``*.scala''}\\ ./src/Pure/General/xml.scala\\ ./src/Pure/General/linear\_set.scala\\ -./src/Pure/General/symbol.scala\\ -./src/Pure/General/exn.scala\\ -./src/Pure/General/position.scala\\ -./src/Pure/General/scan.scala\\ -./src/Pure/General/xml\_data.scala\\ -./src/Pure/General/yxml.scala\\ -./src/Pure/General/markup.scala\\ -./src/Pure/General/sha1.scala\\ +%./src/Pure/General/symbol.scala\\ +%./src/Pure/General/exn.scala\\ +%./src/Pure/General/position.scala\\ +%./src/Pure/General/scan.scala\\ +%./src/Pure/General/xml\_data.scala\\ +%./src/Pure/General/yxml.scala\\ +%./src/Pure/General/markup.scala\\ +:\\ +%./src/Pure/General/sha1.scala\\ ./src/Pure/General/timing.scala\\ ./src/Pure/General/pretty.scala\\ .\\ @@ -196,14 +160,15 @@ .\\ ./src/Pure/System/gui\_setup.scala\\ ./src/Pure/System/isabelle\_system.scala\\ -./src/Pure/System/swing\_thread.scala\\ -./src/Pure/System/download.scala\\ -./src/Pure/System/session\_manager.scala\\ -./src/Pure/System/standard\_system.scala\\ -./src/Pure/System/isabelle\_syntax.scala\\ -./src/Pure/System/session.scala\\ -./src/Pure/System/platform.scala\\ -./src/Pure/System/cygwin.scala\\ +%./src/Pure/System/swing\_thread.scala\\ +%./src/Pure/System/download.scala\\ +%./src/Pure/System/session\_manager.scala\\ +%./src/Pure/System/standard\_system.scala\\ +%./src/Pure/System/isabelle\_syntax.scala\\ +%./src/Pure/System/session.scala\\ +%./src/Pure/System/platform.scala\\ +%./src/Pure/System/cygwin.scala\\ +:\\ ./src/Pure/System/event\_bus.scala\\ ./src/Pure/System/isabelle\_process.scala\\ .\\ @@ -263,7 +228,7 @@ \section[Projektarbeit]{Projekt: Vorarbeiten f\"ur ``structured derivations'' (SD)} \subsection[Aufgabenstellung]{Definition der Aufgabenstellung} \begin{frame}\frametitle{Definition der Aufgabenstellung} -Aufgabenstellung: \\Feasibility-Study zur Implementierung von ``structured derivations'' in Isabelle.\\ +Aufgabenstellung: \\Feasibility-Study zur Implementierung von ``structured~derivations'' (SD) in Isabelle.\\ \textit{``Die Implementierung soweit vorantreiben wie im gegebenen Studenausma\3 m\"oglich~!''}\\ @@ -355,6 +320,49 @@ \end{itemize} \end{frame} +\begin{frame}\frametitle{Sources des jEdit Plugins} +{\tiny +src/Tools/jEditC\textbf{\$ ls -l *}\\ +build.xml\\ +%makedist\\ +%manifest.mf\\ +%README\_BUILD\\ +\textbf{build/*}\\ +\textbf{contrib/*}\\ +\textbf{dist/*}\\ +\textbf{plugin/}build.xml\\ +\textbf{plugin/}changes40.txt\\ +\textbf{plugin/}changes42.txt\\ +\textbf{plugin/}description.html\\ +\textbf{plugin/}IsacActions.java\\ +\textbf{plugin/}Isac.iml\\ +\textbf{plugin/}Isac.java\\ +\textbf{plugin/}IsacOptionPane.java\\ +\textbf{plugin/}IsacPlugin.java\\ +\textbf{plugin/}IsacTextArea.java\\ +\textbf{plugin/}IsacToolPanel.java\\ +\textbf{plugin/}plugin\\ +\textbf{plugin/}README.txt\\ +\textbf{nbproject/*}\\ +\textbf{src/}actions.xml\\ +\textbf{src/}changes40.txt\\ +\textbf{src/}changes42.txt\\ +\textbf{src/}description.html\\ +\textbf{src/}dockables.xml\\ +\textbf{src/}IsacActions.scala\\ +\textbf{src/}Isac.iml\\ +\textbf{src/}IsacOptionPane.scala\\ +\textbf{src/}IsacPlugin.scala\\ +\textbf{src/}Isac.props\\ +\textbf{src/}Isac.scala\\ +\textbf{src/}IsacTextArea.scala\\ +\textbf{src/}IsacToolPanel.scala\\ +\textbf{src/}manifest.mf\\ +\textbf{src/}README.txt\\ +\textbf{src/}users-guide.xml +} +\end{frame} + \begin{frame}\frametitle{Anforderungen an das Versuchs-Plugin} Folgende Funktionalit\"at wurde zu Testzwecken umgesetzt: \pause @@ -378,7 +386,7 @@ \end{frame} -\subsection[Parser]{Ein funktionaler Parser f\"ur SD (in SML)} +%\subsection[Parser]{Ein funktionaler Parser f\"ur SD (in SML)} \section[Summary]{Zusammenfassung} \begin{frame}\frametitle{Zusammenfassung}