1.1 --- a/doc-src/isac/msteger/official_docu/Doku.tex Thu Jun 23 11:29:53 2011 +0200
1.2 +++ b/doc-src/isac/msteger/official_docu/Doku.tex Thu Jun 23 14:51:53 2011 +0200
1.3 @@ -81,14 +81,14 @@
1.4
1.5 \subsection{Isabelle-Pure}
1.6 In diesem Plugin ist der eigentliche CTP-Teil von Isabelle verpackt. Das bedeutet im weiteren Sinn, dass es hier keine grafische Verarbeitung der Daten gibt, sondern der Zugriff von aussen erforderich ist, um den CTP mit Daten zu versorgen und diese nach deren Verabreitung in Isabelle-Pure auszuwerten. Also ist nur hier eine Schnittstelle zum eigentlichen Proofer m\"{o}glich und deshalb ist dieses Plugin f\"{u}r das \sisac-Projekt von zentraler Bedeutung. Standardm\"{a}{\ss}ig ist bereits ein Pure.jar-Paket f\"{u}r jEdit vorhanden. Um SD umsetzten zu k\"{o}nnen, muss hier eine Schnittstelle zu Isabelle-Pure implementiert werden. Nach diesem Schritt kann das Plugin Pure.jar neu gebaut werden.
1.7 -Eine Auflistung der f\"ur das Isabelle-Pure-Packet ben\"otigten Scala-Source-Files kann Anhang B.2 entnommen werden.
1.8 +Eine Auflistung der f\"ur das Isabelle-Pure-Packet ben\"otigten Scala-Source-Filles kann Anhang B.2 entnommen werden.
1.9
1.10 \subsection{Isabelle-jEdit}
1.11 Dieser Teil von Isabelle repr\"{a}sentiert das Frontend in jEdit. Hier wird also die grafische Aufbereitung der von Isabelle-Pure berechneten Daten \"{u}bernommen. Dieses Plugin zeigt sehr sch\"{o}n, wie bereits bestehende Plugins weiter genutzt und erweitert werden k\"{o}nnen.
1.12 An diesem Plugin wird von Seiten der Isabelle-Entwickler sehr stark weitergearbeitet. Darum sollten hier wohl nicht zu viele, am besten nat\"{u}rlich keine \"{A}nderungen, vorgenommen werden. Der Umstand, dass sich einzelne Plugins ganz einfach in einem anderen mitverwenden lassen, macht es m\"{o}glich, dass das \sisac-Plugin sehr einfach, im Idealfall von Seiten der Isabelle-Entwickler, in das Isabelle-jEdit-Plugin integriert werden kann.
1.13
1.14 \subsection{Paketstruktur von Isabelle}
1.15 -Durch die Komplexit\"{a}t des Isabelle-Entwicklungs-Aufbaus soll hier eine Auflistung aller relevanten jar-Pakete erfolgen. Alle Pakete befinden sich innerhalb der Ordnerstruktur von ISABELLE\_HOME. Darum wird ab hier immer von diesem Verzeichnis ausgegangen.
1.16 +pDurch die Komplexit\"{a}t des Isabelle-Entwicklungs-Aufbaus soll hier eine Auflistung aller relevanten jar-Pakete erfolgen. Alle Pakete befinden sich innerhalb der Ordnerstruktur von ISABELLE\_HOME. Darum wird ab hier immer von diesem Verzeichnis ausgegangen.
1.17 Die nachfolgende Auflistung zeigt alle Pakete, die f\"{u}r SD bzw. \sisac von Bedeutung sind und und wo diese zu finden sind.
1.18
1.19
1.20 @@ -141,7 +141,160 @@
1.21 \section{Konfiguration des Netbeans Projektes}
1.22 Um in k\"unftigen Entwicklungsvorhaben effizient kooperieren zu k\"onnen, wurde das Netbeans-Projekt genau nach den Vorgaben des Isabelle-Teams konfiguriert.
1.23
1.24 -TODO
1.25 +\begin{enumerate}
1.26 +\item Konfigurations-Files von Netbeans in ``Files''-View; beeinflussen sich gegenseitig
1.27 + \begin{enumerate}
1.28 + \item build.xml (aus template erzeugt, keine automatischen Ver\"anderunen)
1.29 + \item nbproject/build-impl.xml (z.T. automatische Ver\"anderunen)
1.30 + \item nbproject/project.xml (z.T. automatische Ver\"anderunen)
1.31 + \item TODO
1.32 + \end{enumerate}
1.33 +\item Sacla-plugin installieren laut http://wiki.netbeans.org/Scala69,
1.34 + \begin{enumerate}
1.35 + \item von ``Install with NetBeasn 6.9''
1.36 + \item nach /usr/local/netbeans.../plugins/scala
1.37 + \end{enumerate}
1.38 +\item Scala-plugin installiert in NetBeans
1.39 + \begin{enumerate}
1.40 + \item Men\"u $>$ Tools $>$ Plugins $>$ Downloaded $>$ Add Plugins
1.41 + \item alle Files von /usr/local/netbeans.../plugins/scala/
1.42 + \item Fenster zeigt alle ausgew\"alten Files
1.43 + \item $<$Install$>$ calls Wizzard $<$Next$>$ probably accept Warning
1.44 + \item Funktionstest: Men\"ue $>$ Files $>$ New Project: zeigt Scala als ``Categories''
1.45 + \end{enumerate}
1.46 +\item Neues Projekt ``isac-jedit'' konfigurieren
1.47 + \begin{enumerate}
1.48 + \item Men\"u $>$ Open Project (weil schon aus dem Repository die notwendigen Files vorhanden sind)
1.49 + \item /src/Tools/jeditC: Reference Problems, weil jEdit folgende Plugins braucht
1.50 + \item Funktionskontrolle: ``Projects''-View zeigt das neue Projekt
1.51 + \item Die Konfigurations-Files sind v\"ollig getrennt von anderen Projekten
1.52 + \item Referenz-Probleme beheben; das zeigt auch eventuell fehlende Files
1.53 + \begin{enumerate}
1.54 + \item ``Projects''-View $>$ rightMouse $>$ Resolve Reference Problems: Fenster zeigt dieListe der fehlenden Dateien; $<$Next$>$
1.55 + \item Files holen aus ``Tools'' $>$ Libraries: \"uber Filebrowser aus dem Isabelle\_bundle holen contrib/jEdit---/jars
1.56 + \item ``New Library''
1.57 + \begin{enumerate}
1.58 + \item Cobra-renderer: cobra.jar
1.59 + \item Console: Console.jar
1.60 + \item ErrorList: ErrorList.jar
1.61 + \item Hyperlinks: Hyperlinks.jar
1.62 + \item Isabelle-Pure: Pure.jar
1.63 + \item Rhino-JavaScript: js.jar
1.64 + \item Scala-compiler: scala-compiler.jar
1.65 + \item SideKick: SideKick.jar
1.66 + \end{enumerate}
1.67 + \item Funktions-Kontrollen
1.68 + \begin{enumerate}
1.69 + \item das kleine gelbe Warndreieck im ``Projects''-View ist verschwunden
1.70 + \item im ``Projects''-View 2 Ordner: ``src'' und ``Libraries''
1.71 + \end{enumerate}
1.72 + \end{enumerate}
1.73 + \item jEdit-Paket zum ``isac-jedit''-Projekt hinzuf\"ugen
1.74 + \begin{enumerate}
1.75 + \item ``Project''-View $>$ rightMouse $>$ Add Jar/Folder: Filebrowser
1.76 + \item /contrib/jedit.../jedit.jar
1.77 + \item Funktions-Kontrolle: ist in ``Projects''/Libraries/jedit.jar
1.78 + \end{enumerate}
1.79 + \item Das neue Projekt ``isac-jedit'' zum Hauptprojekt machen: ``Project''-View $>$ rightMouse $>$ Set as Main Project; Funktions-Kontrolle: der Projektname ist boldface.
1.80 + \end{enumerate}
1.81 +\item Ab nun wird die Konfiguration \"uber ``trial and error'' zu Ende gef\"uhrt
1.82 + \begin{enumerate}
1.83 + \item Men\"u $>$ Build Main
1.84 + \begin{enumerate}
1.85 + \item Wenn: Target ``Isac-impl.jar'' does not exist in the project ``isac-jedit''. It is used from target ``debug''
1.86 + \begin{enumerate}
1.87 + \item Versuch
1.88 + \begin{itemize}
1.89 + \item build-impl.xml l\"oschen
1.90 + \item NetBeans neu starten, stellt build-impl.xml automatisch aus build.xml wieder her
1.91 + \item \dots hat in diesem Fall nicht geholfen
1.92 + \end{itemize}
1.93 + \item Versuch zur Vermutung: Projekt wurde umbenannt von ``Isac'' in ``isac-jedit'', und das machte build.xml inkonsistent
1.94 + \begin{itemize}
1.95 + \item in build.xml query-replace ``Isac'' in ``isac-jedit''
1.96 + \item TODO?
1.97 + \item
1.98 + \end{itemize}
1.99 + \end{enumerate}
1.100 + \item Wenn: Problem: failed to create tsk or type scalac
1.101 + \begin{enumerate}
1.102 + \item Versuch: Pfad zum Scala bekanntgeben
1.103 + \begin{itemize}
1.104 + \item /usr/local/netbeans-6.9.1/etc/netbeans.conf: netbeans\_default\_options= richtigen Scala-Pfad setzen
1.105 + \item build-impl.xml l\"oschen
1.106 + \item NetBeans neu starten.
1.107 + \end{itemize}
1.108 + \end{enumerate}
1.109 + \item Wenn Fehler: ``/usr/local/isabisac/src/Tools/jEditC/\${project.jEdit}/modes does not exist''
1.110 + \begin{enumerate}
1.111 + \item grep -r "project.jEdit" *
1.112 + \item nbproject/project.properties:project.jEdit=contrib/jEdit
1.113 + \item
1.114 + \item
1.115 +
1.116 + \begin{itemize}
1.117 + \item
1.118 + \begin{itemize}
1.119 + \item
1.120 + \item
1.121 + \item
1.122 + \end{itemize}
1.123 + \item
1.124 + \item
1.125 + \end{itemize}
1.126 + \item
1.127 + \item
1.128 + \end{enumerate}
1.129 + \item
1.130 + \item
1.131 + \end{enumerate}
1.132 + \end{enumerate}
1.133 +$<$ $>$
1.134 +Men\"u $>$ $>$ $>$ $>$ $>$ $>$
1.135 +``Project''-View $>$ rightMouse $>$ $>$ $>$ $>$ $>$
1.136 +\item
1.137 + \begin{enumerate}
1.138 + \item
1.139 + \begin{enumerate}
1.140 + \item
1.141 + \begin{itemize}
1.142 + \item
1.143 + \begin{itemize}
1.144 + \item
1.145 + \item
1.146 + \item
1.147 + \end{itemize}
1.148 + \item
1.149 + \item
1.150 + \end{itemize}
1.151 + \item
1.152 + \item
1.153 + \end{enumerate}
1.154 + \item
1.155 + \item
1.156 + \end{enumerate}
1.157 +\item
1.158 + \begin{enumerate}
1.159 + \item
1.160 + \begin{enumerate}
1.161 + \item
1.162 + \begin{itemize}
1.163 + \item
1.164 + \begin{itemize}
1.165 + \item
1.166 + \item
1.167 + \item
1.168 + \end{itemize}
1.169 + \item
1.170 + \item
1.171 + \end{itemize}
1.172 + \item
1.173 + \item
1.174 + \end{enumerate}
1.175 + \item
1.176 + \item
1.177 + \end{enumerate}
1.178 +\end{enumerate}
1.179
1.180
1.181 \section{Implementation der jEdit Komponenten}