1.1 --- a/doc-src/isac/mlehnfeld/presentation.tex	Sat May 28 02:55:36 2011 +0200
     1.2 +++ b/doc-src/isac/mlehnfeld/presentation.tex	Sat May 28 21:41:12 2011 +0200
     1.3 @@ -157,11 +157,12 @@
     1.4      \item theories too general
     1.5      \item not capable of type inference
     1.6      \item replace function \texttt{parseNEW}
     1.7 +    \item assumptions \& environment $\rightarrow$ context
     1.8      \end{itemize}
     1.9  \end{frame}
    1.10  
    1.11  \begin{frame}
    1.12 -  \frametitle{Introduction of Isabelle Contexts}
    1.13 +  \frametitle{Code Snippets: \texttt{parse}}
    1.14      \texttt{\tiny{
    1.15        \begin{tabbing}
    1.16  xx\=xx\=xx\=xx\=\kill
    1.17 @@ -173,12 +174,41 @@
    1.18  \\~\\~\\
    1.19  fun parseNEW ctxt str = SOME (Syntax.read\_term ctxt str |> numbers\_to\_string)\\
    1.20  \>\>\>handle \_ => NONE;
    1.21 -\\~\\~\\
    1.22 +      \end{tabbing}
    1.23 +    }}
    1.24 +\end{frame}
    1.25 +
    1.26 +
    1.27 +\begin{frame}
    1.28 +  \frametitle{Code Snippets: context data}
    1.29 +    \texttt{\tiny{
    1.30 +      \begin{tabbing}
    1.31 +xx\=xx\=xx\=xx\=\kill
    1.32 +datatype Isac\_Ctxt =\\
    1.33 +\>\>Env of term * term\\
    1.34 +\>| Asm of term;\\
    1.35 +\\
    1.36 +structure ContextData = Proof\_Data\\
    1.37 +\>~(type T = Isac\_Ctxt list\\
    1.38 +\>\>fun init \_ = []);\\
    1.39 +\\
    1.40  local\\
    1.41  \>fun insert\_ctxt data = ContextData.map (fn xs => distinct (data@xs));\\
    1.42  in\\
    1.43  \>fun insert\_assumptions asms = map (fn t => Asm t) asms |> insert\_ctxt;\\
    1.44  \>fun insert\_environments envs = map (fn t => Env t) envs |> insert\_ctxt;\\
    1.45 +end\\
    1.46 +\\
    1.47 +local\\
    1.48 +\>fun unpack\_asms (Asm t::ts) = t::(unpack\_asms ts)\\
    1.49 +\>\>| unpack\_asms (Env \_::ts) = unpack\_asms ts\\
    1.50 +\>\>| unpack\_asms [] = [];\\
    1.51 +\>fun unpack\_envs (Env t::ts) = t::(unpack\_envs ts)\\
    1.52 +\>\>| unpack\_envs (Asm \_::ts) = unpack\_envs ts\\
    1.53 +\>\>| unpack\_envs [] = [];\\
    1.54 +in\\
    1.55 +\>fun get\_assumptions ctxt = ContextData.get ctxt |> unpack\_asms;\\
    1.56 +\>fun get\_environments ctxt = ContextData.get ctxt |> unpack\_envs;\\
    1.57  end
    1.58        \end{tabbing}
    1.59      }}
    1.60 @@ -186,7 +216,7 @@
    1.61  
    1.62  \subsection[Redesign]{Redesign of Type Inference in \isac}
    1.63  \begin{frame}
    1.64 -  \frametitle{Redesign of type inference in \isac}
    1.65 +  \frametitle{Redesign of Type Inference in \isac}
    1.66      \begin{itemize}
    1.67      \item use context type inference
    1.68      \item parsing input (specification \& user input)
    1.69 @@ -195,6 +225,18 @@
    1.70      \end{itemize}
    1.71  \end{frame}
    1.72  
    1.73 +\begin{frame}
    1.74 +  \frametitle{Lines of Code}
    1.75 +    \begin{tabular}{lr}
    1.76 +      src/ & 1700 k \\
    1.77 +      src/Pure/ & 70 k \\
    1.78 +      src/Provers/ & 8 k \\
    1.79 +      src/Tools/ & 800 k \\
    1.80 +      src/isac/ & 37 k \\
    1.81 +      src/isac/Knowledge & 16 k \\
    1.82 +    \end{tabular}
    1.83 +\end{frame}
    1.84 +
    1.85  \subsection[Code Improvement]{Improvement of functional code}
    1.86  \begin{frame}
    1.87    \frametitle{Improvement of functional code}
    1.88 @@ -265,13 +307,18 @@
    1.89      \end{itemize}
    1.90  \end{frame}
    1.91  
    1.92 +\begin{frame}
    1.93 +  \frametitle{jedit demonstration}
    1.94 +  DEMO
    1.95 +\end{frame}
    1.96 +
    1.97  \section[Problems]{Problems encountered in the project}
    1.98  \begin{frame}
    1.99    \frametitle{Problems encountered in the project}
   1.100      \begin{itemize}
   1.101      \item publication of new Isabelle release
   1.102      \item amount of code in Isabelle and \isac
   1.103 -    \item changes scattered throughout the code
   1.104 +    \item changes scattered throughout the code ($\rightarrow$ grep)
   1.105      \end{itemize}
   1.106  \end{frame}
   1.107