doc-src/isac/msteger/bakk-presentation.tex
branchdecompose-isar
changeset 42048 6548da70f14e
parent 42046 bb864b8144a3
child 42050 2b69a774afd5
     1.1 --- a/doc-src/isac/msteger/bakk-presentation.tex	Sat Jun 18 11:28:10 2011 +0200
     1.2 +++ b/doc-src/isac/msteger/bakk-presentation.tex	Mon Jun 20 17:33:06 2011 +0200
     1.3 @@ -124,57 +124,21 @@
     1.4  \end{frame}
     1.5  
     1.6  \subsection[Integration]{Isabelles Filestruktur im \"Ubergangsstadium}
     1.7 -\begin{frame}\frametitle{Isabelle Files: *.jar}
     1.8 -{\footnotesize
     1.9 ------ for ``isabelle jedit \&''; contained in Isabelle\_bundle}\\
    1.10 -{\tiny
    1.11 -./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jedit.jar\\
    1.12 -./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/LatestVersion.jar\\
    1.13 -./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/SideKick.jar\\
    1.14 -./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/Console.jar\\
    1.15 -./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/Pure.jar \alert{$\;\;\;\;\;\;\;\;\;\;\;\Longleftarrow$ entry to SML}\\
    1.16 -./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/Isac.jar\\
    1.17 -./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/scala-compiler.jar\\
    1.18 -./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/Isabelle-jEdit.jar\\
    1.19 -./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/cobra.jar\\
    1.20 -./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/js.jar\\
    1.21 -./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/Hyperlinks.jar\\
    1.22 -./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/scala-swing.jar\\
    1.23 -./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/scala-library.jar\\
    1.24 -./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/QuickNotepad.jar\\
    1.25 -./contrib/jedit-4.3.2\_Isabelle-6d736d983d5c/jars/ErrorList.jar\\
    1.26 -
    1.27 -{\footnotesize
    1.28 ------ scala system; contained in Isabelle\_bundle}\\
    1.29 -./contrib/scala-2.8.1.final/misc/sbaz/scala-bazaars.jar\\
    1.30 -./contrib/scala-2.8.1.final/misc/sbaz/sbaz-tests.jar\\
    1.31 -./contrib/scala-2.8.1.final/misc/scala-devel/plugins/continuations.jar\\
    1.32 -./contrib/scala-2.8.1.final/lib/scala-compiler.jar\\
    1.33 -./contrib/scala-2.8.1.final/lib/scalap.jar\\
    1.34 -./contrib/scala-2.8.1.final/lib/scala-swing.jar\\
    1.35 -./contrib/scala-2.8.1.final/lib/scala-library.jar\\
    1.36 -./contrib/scala-2.8.1.final/lib/jline.jar\\
    1.37 -./contrib/scala-2.8.1.final/lib/scala-dbc.jar\\
    1.38 -./contrib/scala-2.8.1.final/src/scala-library-src.jar\\
    1.39 -./contrib/scala-2.8.1.final/src/scala-swing-src.jar\\
    1.40 -./contrib/scala-2.8.1.final/src/scala-compiler-src.jar\\
    1.41 -./contrib/scala-2.8.1.final/src/scala-dbc-src.jar\\
    1.42 -./contrib/scala-2.8.1.final/src/sbaz-src.jar\\
    1.43 -}
    1.44 -\end{frame}
    1.45  
    1.46  \begin{frame}\frametitle{Isabelle Files: *.scala}
    1.47  {\tiny
    1.48 +\textbf{\$ find -name ``*.scala''}\\
    1.49  ./src/Pure/General/xml.scala\\
    1.50  ./src/Pure/General/linear\_set.scala\\
    1.51 -./src/Pure/General/symbol.scala\\
    1.52 -./src/Pure/General/exn.scala\\
    1.53 -./src/Pure/General/position.scala\\
    1.54 -./src/Pure/General/scan.scala\\
    1.55 -./src/Pure/General/xml\_data.scala\\
    1.56 -./src/Pure/General/yxml.scala\\
    1.57 -./src/Pure/General/markup.scala\\
    1.58 -./src/Pure/General/sha1.scala\\
    1.59 +%./src/Pure/General/symbol.scala\\
    1.60 +%./src/Pure/General/exn.scala\\
    1.61 +%./src/Pure/General/position.scala\\
    1.62 +%./src/Pure/General/scan.scala\\
    1.63 +%./src/Pure/General/xml\_data.scala\\
    1.64 +%./src/Pure/General/yxml.scala\\
    1.65 +%./src/Pure/General/markup.scala\\
    1.66 +:\\
    1.67 +%./src/Pure/General/sha1.scala\\
    1.68  ./src/Pure/General/timing.scala\\
    1.69  ./src/Pure/General/pretty.scala\\
    1.70  .\\
    1.71 @@ -196,14 +160,15 @@
    1.72  .\\
    1.73  ./src/Pure/System/gui\_setup.scala\\
    1.74  ./src/Pure/System/isabelle\_system.scala\\
    1.75 -./src/Pure/System/swing\_thread.scala\\
    1.76 -./src/Pure/System/download.scala\\
    1.77 -./src/Pure/System/session\_manager.scala\\
    1.78 -./src/Pure/System/standard\_system.scala\\
    1.79 -./src/Pure/System/isabelle\_syntax.scala\\
    1.80 -./src/Pure/System/session.scala\\
    1.81 -./src/Pure/System/platform.scala\\
    1.82 -./src/Pure/System/cygwin.scala\\
    1.83 +%./src/Pure/System/swing\_thread.scala\\
    1.84 +%./src/Pure/System/download.scala\\
    1.85 +%./src/Pure/System/session\_manager.scala\\
    1.86 +%./src/Pure/System/standard\_system.scala\\
    1.87 +%./src/Pure/System/isabelle\_syntax.scala\\
    1.88 +%./src/Pure/System/session.scala\\
    1.89 +%./src/Pure/System/platform.scala\\
    1.90 +%./src/Pure/System/cygwin.scala\\
    1.91 +:\\
    1.92  ./src/Pure/System/event\_bus.scala\\
    1.93  ./src/Pure/System/isabelle\_process.scala\\
    1.94  .\\
    1.95 @@ -263,7 +228,7 @@
    1.96  \section[Projektarbeit]{Projekt: Vorarbeiten f\"ur ``structured derivations'' (SD)}
    1.97  \subsection[Aufgabenstellung]{Definition der Aufgabenstellung}
    1.98  \begin{frame}\frametitle{Definition der Aufgabenstellung}
    1.99 -Aufgabenstellung: \\Feasibility-Study zur Implementierung von ``structured derivations'' in Isabelle.\\
   1.100 +Aufgabenstellung: \\Feasibility-Study zur Implementierung von ``structured~derivations'' (SD) in Isabelle.\\
   1.101  
   1.102  \textit{``Die Implementierung soweit vorantreiben wie im gegebenen Studenausma\3 m\"oglich~!''}\\
   1.103  
   1.104 @@ -355,6 +320,49 @@
   1.105  \end{itemize}
   1.106  \end{frame}
   1.107  
   1.108 +\begin{frame}\frametitle{Sources des jEdit Plugins}
   1.109 +{\tiny
   1.110 +src/Tools/jEditC\textbf{\$ ls -l *}\\
   1.111 +build.xml\\
   1.112 +%makedist\\
   1.113 +%manifest.mf\\
   1.114 +%README\_BUILD\\
   1.115 +\textbf{build/*}\\
   1.116 +\textbf{contrib/*}\\
   1.117 +\textbf{dist/*}\\
   1.118 +\textbf{plugin/}build.xml\\
   1.119 +\textbf{plugin/}changes40.txt\\
   1.120 +\textbf{plugin/}changes42.txt\\
   1.121 +\textbf{plugin/}description.html\\
   1.122 +\textbf{plugin/}IsacActions.java\\
   1.123 +\textbf{plugin/}Isac.iml\\
   1.124 +\textbf{plugin/}Isac.java\\
   1.125 +\textbf{plugin/}IsacOptionPane.java\\
   1.126 +\textbf{plugin/}IsacPlugin.java\\
   1.127 +\textbf{plugin/}IsacTextArea.java\\
   1.128 +\textbf{plugin/}IsacToolPanel.java\\
   1.129 +\textbf{plugin/}plugin\\
   1.130 +\textbf{plugin/}README.txt\\
   1.131 +\textbf{nbproject/*}\\
   1.132 +\textbf{src/}actions.xml\\
   1.133 +\textbf{src/}changes40.txt\\
   1.134 +\textbf{src/}changes42.txt\\
   1.135 +\textbf{src/}description.html\\
   1.136 +\textbf{src/}dockables.xml\\
   1.137 +\textbf{src/}IsacActions.scala\\
   1.138 +\textbf{src/}Isac.iml\\
   1.139 +\textbf{src/}IsacOptionPane.scala\\
   1.140 +\textbf{src/}IsacPlugin.scala\\
   1.141 +\textbf{src/}Isac.props\\
   1.142 +\textbf{src/}Isac.scala\\
   1.143 +\textbf{src/}IsacTextArea.scala\\
   1.144 +\textbf{src/}IsacToolPanel.scala\\
   1.145 +\textbf{src/}manifest.mf\\
   1.146 +\textbf{src/}README.txt\\
   1.147 +\textbf{src/}users-guide.xml
   1.148 +}
   1.149 +\end{frame}
   1.150 +
   1.151  \begin{frame}\frametitle{Anforderungen an das Versuchs-Plugin}
   1.152  Folgende Funktionalit\"at wurde zu Testzwecken umgesetzt:
   1.153  \pause
   1.154 @@ -378,7 +386,7 @@
   1.155  \end{frame}
   1.156  
   1.157  
   1.158 -\subsection[Parser]{Ein funktionaler Parser f\"ur SD (in SML)}
   1.159 +%\subsection[Parser]{Ein funktionaler Parser f\"ur SD (in SML)}
   1.160  
   1.161  \section[Summary]{Zusammenfassung}
   1.162  \begin{frame}\frametitle{Zusammenfassung}