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}

     2.1 --- a/src/Tools/jEditC/hs_err_pid5529.log	Sat Jun 18 11:28:10 2011 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,396 +0,0 @@
     2.4 -#
     2.5 -# A fatal error has been detected by the Java Runtime Environment:
     2.6 -#
     2.7 -#  SIGSEGV (0xb) at pc=0xb499496b, pid=5529, tid=3078630256
     2.8 -#
     2.9 -# JRE version: 6.0_20-b20
    2.10 -# Java VM: OpenJDK Server VM (19.0-b09 mixed mode linux-x86 )
    2.11 -# Derivative: IcedTea6 1.9.4
    2.12 -# Distribution: Ubuntu 10.04.1 LTS, package 6b20-1.9.4-0ubuntu1~10.04.1
    2.13 -# Problematic frame:
    2.14 -# J  scala.tools.nsc.transform.UnCurry$$anon$3.apply(Lscala/tools/nsc/symtab/Types$Type;)Lscala/tools/nsc/symtab/Types$Type;
    2.15 -#
    2.16 -# If you would like to submit a bug report, please include
    2.17 -# instructions how to reproduce the bug and visit:
    2.18 -#   https://bugs.launchpad.net/ubuntu/+source/openjdk-6/
    2.19 -#
    2.20 -
    2.21 ----------------  T H R E A D  ---------------
    2.22 -
    2.23 -Current thread (0x0813e400):  JavaThread "main" [_thread_in_Java, id=5532, stack(0xb77b2000,0xb7803000)]
    2.24 -
    2.25 -siginfo:si_signo=SIGSEGV: si_errno=0, si_code=128 (), si_addr=0x00000000
    2.26 -
    2.27 -Registers:
    2.28 -EAX=0x95763760, EBX=0x955105b8, ECX=0x9586cf98, EDX=0x95763760
    2.29 -ESP=0xb7800f10, EBP=0x9586cf58, ESI=0xb7800f6c, EDI=0x9586cf58
    2.30 -EIP=0xb499496b, CR2=0x00000008, EFLAGS=0x00210206
    2.31 -
    2.32 -Register to memory mapping:
    2.33 -
    2.34 -EAX=0x95763760
    2.35 -scala.tools.nsc.symtab.Types$TypeRef$rawTypeRef$1 
    2.36 - - klass: 'scala/tools/nsc/symtab/Types$TypeRef$rawTypeRef$1'
    2.37 -
    2.38 -EBX=0x955105b8
    2.39 -scala.tools.nsc.symtab.Symbols$ClassSymbol 
    2.40 - - klass: 'scala/tools/nsc/symtab/Symbols$ClassSymbol'
    2.41 -
    2.42 -ECX=0x9586cf98
    2.43 -scala.tools.nsc.transform.UnCurry$$anon$3 
    2.44 - - klass: 'scala/tools/nsc/transform/UnCurry$$anon$3'
    2.45 -
    2.46 -EDX=0x95763760
    2.47 -scala.tools.nsc.symtab.Types$TypeRef$rawTypeRef$1 
    2.48 - - klass: 'scala/tools/nsc/symtab/Types$TypeRef$rawTypeRef$1'
    2.49 -
    2.50 -ESP=0xb7800f10
    2.51 -0xb7800f10 is pointing into the stack for thread: 0x0813e400
    2.52 -"main" prio=10 tid=0x0813e400 nid=0x159c runnable [0x00000000]
    2.53 -   java.lang.Thread.State: RUNNABLE
    2.54 -
    2.55 -EBP=0x9586cf58
    2.56 -scala.tools.nsc.Global$uncurry$ 
    2.57 - - klass: 'scala/tools/nsc/Global$uncurry$'
    2.58 -
    2.59 -ESI=0xb7800f6c
    2.60 -0xb7800f6c is pointing into the stack for thread: 0x0813e400
    2.61 -"main" prio=10 tid=0x0813e400 nid=0x159c runnable [0x00000000]
    2.62 -   java.lang.Thread.State: RUNNABLE
    2.63 -
    2.64 -EDI=0x9586cf58
    2.65 -scala.tools.nsc.Global$uncurry$ 
    2.66 - - klass: 'scala/tools/nsc/Global$uncurry$'
    2.67 -
    2.68 -
    2.69 -Top of Stack: (sp=0xb7800f10)
    2.70 -0xb7800f10:   948dd5f8 955d5430 9586cf98 9586cf58
    2.71 -0xb7800f20:   9480b4a0 957637a8 948e21c8 95b761e8
    2.72 -0xb7800f30:   95763760 95b761e8 00b6e39f 0813e400
    2.73 -0xb7800f40:   8c2f8818 b7800f74 8ce92f40 b480aaf0
    2.74 -0xb7800f50:   b7800f70 8d0aa7a0 b7800f94 b47b5523
    2.75 -0xb7800f60:   00000000 b7800f70 b47b5523 95763760
    2.76 -0xb7800f70:   9586cf98 b7800f74 8d65624f b7800fa8
    2.77 -0xb7800f80:   8d6568d8 8d820a68 8d6562b0 b7800f6c 
    2.78 -
    2.79 -Instructions: (pc=0xb499496b)
    2.80 -0xb499495b:   8c 0f 84 9b 09 00 00 8b 4c 24 08 8b 54 24 20 90
    2.81 -0xb499496b:   e8 5c 27 0a 00 89 44 24 08 85 ed 0f 84 71 09 00 
    2.82 -
    2.83 -Stack: [0xb77b2000,0xb7803000],  sp=0xb7800f10,  free space=315k
    2.84 -Native frames: (J=compiled Java code, j=interpreted, Vv=VM code, C=native code)
    2.85 -J  scala.tools.nsc.transform.UnCurry$$anon$3.apply(Lscala/tools/nsc/symtab/Types$Type;)Lscala/tools/nsc/symtab/Types$Type;
    2.86 -
    2.87 -
    2.88 ----------------  P R O C E S S  ---------------
    2.89 -
    2.90 -Java Threads: ( => current thread )
    2.91 -  0x8c296800 JavaThread "Low Memory Detector" daemon [_thread_blocked, id=5541, stack(0x8bde5000,0x8be36000)]
    2.92 -  0x8c294c00 JavaThread "CompilerThread1" daemon [_thread_in_native, id=5540, stack(0x8be36000,0x8beb7000)]
    2.93 -  0x8c292800 JavaThread "CompilerThread0" daemon [_thread_in_native, id=5539, stack(0x8beb7000,0x8bf38000)]
    2.94 -  0x8c291000 JavaThread "Signal Dispatcher" daemon [_thread_blocked, id=5538, stack(0x8bf38000,0x8bf89000)]
    2.95 -  0x8c281000 JavaThread "Finalizer" daemon [_thread_blocked, id=5537, stack(0x8bfcf000,0x8c020000)]
    2.96 -  0x8c27f800 JavaThread "Reference Handler" daemon [_thread_blocked, id=5536, stack(0x8c020000,0x8c071000)]
    2.97 -=>0x0813e400 JavaThread "main" [_thread_in_Java, id=5532, stack(0xb77b2000,0xb7803000)]
    2.98 -
    2.99 -Other Threads:
   2.100 -  0x8c27bc00 VMThread [stack: 0x8c30f000,0x8c390000] [id=5535]
   2.101 -  0x8c298c00 WatcherThread [stack: 0x8bd64000,0x8bde5000] [id=5542]
   2.102 -
   2.103 -VM state:not at safepoint (normal execution)
   2.104 -
   2.105 -VM Mutex/Monitor currently owned by a thread: None
   2.106 -
   2.107 -Heap
   2.108 - PSYoungGen      total 84864K, used 34429K [0xa9c50000, 0xaf7a0000, 0xb46f0000)
   2.109 -  eden space 76224K, 45% used [0xa9c50000,0xabdef708,0xae6c0000)
   2.110 -  from space 8640K, 0% used [0xaef30000,0xaef30000,0xaf7a0000)
   2.111 -  to   space 8640K, 0% used [0xae6c0000,0xae6c0000,0xaef30000)
   2.112 - PSOldGen        total 36352K, used 21119K [0x946f0000, 0x96a70000, 0xa9c50000)
   2.113 -  object space 36352K, 58% used [0x946f0000,0x95b8ffe8,0x96a70000)
   2.114 - PSPermGen       total 35328K, used 19196K [0x8c6f0000, 0x8e970000, 0x946f0000)
   2.115 -  object space 35328K, 54% used [0x8c6f0000,0x8d9af0a0,0x8e970000)
   2.116 -
   2.117 -Dynamic libraries:
   2.118 -00110000-00117000 r-xp 00000000 08:05 2367999    /lib/tls/i686/cmov/librt-2.11.1.so
   2.119 -00117000-00118000 r--p 00006000 08:05 2367999    /lib/tls/i686/cmov/librt-2.11.1.so
   2.120 -00118000-00119000 rw-p 00007000 08:05 2367999    /lib/tls/i686/cmov/librt-2.11.1.so
   2.121 -00119000-00123000 r-xp 00000000 08:05 2367987    /lib/tls/i686/cmov/libnss_files-2.11.1.so
   2.122 -00123000-00124000 r--p 00009000 08:05 2367987    /lib/tls/i686/cmov/libnss_files-2.11.1.so
   2.123 -00124000-00125000 rw-p 0000a000 08:05 2367987    /lib/tls/i686/cmov/libnss_files-2.11.1.so
   2.124 -00163000-00187000 r-xp 00000000 08:05 2367994    /lib/tls/i686/cmov/libm-2.11.1.so
   2.125 -00187000-00188000 r--p 00023000 08:05 2367994    /lib/tls/i686/cmov/libm-2.11.1.so
   2.126 -00188000-00189000 rw-p 00024000 08:05 2367994    /lib/tls/i686/cmov/libm-2.11.1.so
   2.127 -00189000-0019d000 r-xp 00000000 08:05 1447999    /usr/lib/jvm/java-6-openjdk/jre/lib/i386/libnet.so
   2.128 -0019d000-0019e000 r--p 00013000 08:05 1447999    /usr/lib/jvm/java-6-openjdk/jre/lib/i386/libnet.so
   2.129 -0019e000-0019f000 rw-p 00014000 08:05 1447999    /usr/lib/jvm/java-6-openjdk/jre/lib/i386/libnet.so
   2.130 -0021a000-0023e000 r-xp 00000000 08:05 1447986    /usr/lib/jvm/java-6-openjdk/jre/lib/i386/libjava.so
   2.131 -0023e000-0023f000 r--p 00023000 08:05 1447986    /usr/lib/jvm/java-6-openjdk/jre/lib/i386/libjava.so
   2.132 -0023f000-00241000 rw-p 00024000 08:05 1447986    /usr/lib/jvm/java-6-openjdk/jre/lib/i386/libjava.so
   2.133 -00286000-0028c000 r-xp 00000000 08:05 2368006    /lib/tls/i686/cmov/libnss_compat-2.11.1.so
   2.134 -0028c000-0028d000 r--p 00006000 08:05 2368006    /lib/tls/i686/cmov/libnss_compat-2.11.1.so
   2.135 -0028d000-0028e000 rw-p 00007000 08:05 2368006    /lib/tls/i686/cmov/libnss_compat-2.11.1.so
   2.136 -00534000-00687000 r-xp 00000000 08:05 2367991    /lib/tls/i686/cmov/libc-2.11.1.so
   2.137 -00687000-00688000 ---p 00153000 08:05 2367991    /lib/tls/i686/cmov/libc-2.11.1.so
   2.138 -00688000-0068a000 r--p 00153000 08:05 2367991    /lib/tls/i686/cmov/libc-2.11.1.so
   2.139 -0068a000-0068b000 rw-p 00155000 08:05 2367991    /lib/tls/i686/cmov/libc-2.11.1.so
   2.140 -0068b000-0068e000 rw-p 00000000 00:00 0 
   2.141 -0081c000-0081f000 r-xp 00000000 08:05 1447967    /usr/lib/jvm/java-6-openjdk/jre/lib/i386/jli/libjli.so
   2.142 -0081f000-00820000 r--p 00003000 08:05 1447967    /usr/lib/jvm/java-6-openjdk/jre/lib/i386/jli/libjli.so
   2.143 -00820000-00821000 rw-p 00004000 08:05 1447967    /usr/lib/jvm/java-6-openjdk/jre/lib/i386/jli/libjli.so
   2.144 -00944000-0094b000 r-xp 00000000 08:05 1448000    /usr/lib/jvm/java-6-openjdk/jre/lib/i386/libnio.so
   2.145 -0094b000-0094c000 r--p 00006000 08:05 1448000    /usr/lib/jvm/java-6-openjdk/jre/lib/i386/libnio.so
   2.146 -0094c000-0094d000 rw-p 00007000 08:05 1448000    /usr/lib/jvm/java-6-openjdk/jre/lib/i386/libnio.so
   2.147 -00a35000-00a3c000 r-xp 00000000 08:05 1448009    /usr/lib/jvm/java-6-openjdk/jre/lib/i386/libzip.so
   2.148 -00a3c000-00a3d000 r--p 00006000 08:05 1448009    /usr/lib/jvm/java-6-openjdk/jre/lib/i386/libzip.so
   2.149 -00a3d000-00a3e000 rw-p 00007000 08:05 1448009    /usr/lib/jvm/java-6-openjdk/jre/lib/i386/libzip.so
   2.150 -00a8f000-00a96000 r-xp 00000000 08:05 1448010    /usr/lib/jvm/java-6-openjdk/jre/lib/i386/native_threads/libhpi.so
   2.151 -00a96000-00a97000 r--p 00006000 08:05 1448010    /usr/lib/jvm/java-6-openjdk/jre/lib/i386/native_threads/libhpi.so
   2.152 -00a97000-00a98000 rw-p 00007000 08:05 1448010    /usr/lib/jvm/java-6-openjdk/jre/lib/i386/native_threads/libhpi.so
   2.153 -00acb000-00acd000 r-xp 00000000 08:05 2367985    /lib/tls/i686/cmov/libdl-2.11.1.so
   2.154 -00acd000-00ace000 r--p 00001000 08:05 2367985    /lib/tls/i686/cmov/libdl-2.11.1.so
   2.155 -00ace000-00acf000 rw-p 00002000 08:05 2367985    /lib/tls/i686/cmov/libdl-2.11.1.so
   2.156 -00b01000-00b02000 r-xp 00000000 00:00 0          [vdso]
   2.157 -00b26000-00b32000 r-xp 00000000 08:05 1448008    /usr/lib/jvm/java-6-openjdk/jre/lib/i386/libverify.so
   2.158 -00b32000-00b33000 r--p 0000b000 08:05 1448008    /usr/lib/jvm/java-6-openjdk/jre/lib/i386/libverify.so
   2.159 -00b33000-00b34000 rw-p 0000c000 08:05 1448008    /usr/lib/jvm/java-6-openjdk/jre/lib/i386/libverify.so
   2.160 -00cad000-00cc2000 r-xp 00000000 08:05 2367986    /lib/tls/i686/cmov/libpthread-2.11.1.so
   2.161 -00cc2000-00cc3000 r--p 00014000 08:05 2367986    /lib/tls/i686/cmov/libpthread-2.11.1.so
   2.162 -00cc3000-00cc4000 rw-p 00015000 08:05 2367986    /lib/tls/i686/cmov/libpthread-2.11.1.so
   2.163 -00cc4000-00cc6000 rw-p 00000000 00:00 0 
   2.164 -00d40000-00d53000 r-xp 00000000 08:05 2359494    /lib/libz.so.1.2.3.3
   2.165 -00d53000-00d54000 r--p 00012000 08:05 2359494    /lib/libz.so.1.2.3.3
   2.166 -00d54000-00d55000 rw-p 00013000 08:05 2359494    /lib/libz.so.1.2.3.3
   2.167 -00e0e000-00e16000 r-xp 00000000 08:05 2368007    /lib/tls/i686/cmov/libnss_nis-2.11.1.so
   2.168 -00e16000-00e17000 r--p 00007000 08:05 2368007    /lib/tls/i686/cmov/libnss_nis-2.11.1.so
   2.169 -00e17000-00e18000 rw-p 00008000 08:05 2368007    /lib/tls/i686/cmov/libnss_nis-2.11.1.so
   2.170 -00ebc000-00ecf000 r-xp 00000000 08:05 2359410    /lib/tls/i686/cmov/libnsl-2.11.1.so
   2.171 -00ecf000-00ed0000 r--p 00012000 08:05 2359410    /lib/tls/i686/cmov/libnsl-2.11.1.so
   2.172 -00ed0000-00ed1000 rw-p 00013000 08:05 2359410    /lib/tls/i686/cmov/libnsl-2.11.1.so
   2.173 -00ed1000-00ed3000 rw-p 00000000 00:00 0 
   2.174 -00fe0000-00ffb000 r-xp 00000000 08:05 2359672    /lib/ld-2.11.1.so
   2.175 -00ffb000-00ffc000 r--p 0001a000 08:05 2359672    /lib/ld-2.11.1.so
   2.176 -00ffc000-00ffd000 rw-p 0001b000 08:05 2359672    /lib/ld-2.11.1.so
   2.177 -00ffd000-016af000 r-xp 00000000 08:05 1448011    /usr/lib/jvm/java-6-openjdk/jre/lib/i386/server/libjvm.so
   2.178 -016af000-016b0000 ---p 006b2000 08:05 1448011    /usr/lib/jvm/java-6-openjdk/jre/lib/i386/server/libjvm.so
   2.179 -016b0000-016f5000 r--p 006b2000 08:05 1448011    /usr/lib/jvm/java-6-openjdk/jre/lib/i386/server/libjvm.so
   2.180 -016f5000-01704000 rw-p 006f7000 08:05 1448011    /usr/lib/jvm/java-6-openjdk/jre/lib/i386/server/libjvm.so
   2.181 -01704000-01b23000 rw-p 00000000 00:00 0 
   2.182 -08048000-08051000 r-xp 00000000 08:05 1463022    /usr/lib/jvm/java-6-openjdk/jre/bin/java
   2.183 -08051000-08052000 r--p 00008000 08:05 1463022    /usr/lib/jvm/java-6-openjdk/jre/bin/java
   2.184 -08052000-08053000 rw-p 00009000 08:05 1463022    /usr/lib/jvm/java-6-openjdk/jre/bin/java
   2.185 -08138000-08ec2000 rw-p 00000000 00:00 0          [heap]
   2.186 -89d00000-89df9000 rw-p 00000000 00:00 0 
   2.187 -89df9000-89e00000 ---p 00000000 00:00 0 
   2.188 -89f00000-89ffb000 rw-p 00000000 00:00 0 
   2.189 -89ffb000-8a000000 ---p 00000000 00:00 0 
   2.190 -8a100000-8a17f000 rw-p 00000000 00:00 0 
   2.191 -8a17f000-8a200000 ---p 00000000 00:00 0 
   2.192 -8a300000-8a3f5000 rw-p 00000000 00:00 0 
   2.193 -8a3f5000-8a400000 ---p 00000000 00:00 0 
   2.194 -8a400000-8a4f8000 rw-p 00000000 00:00 0 
   2.195 -8a4f8000-8a500000 ---p 00000000 00:00 0 
   2.196 -8a500000-8a5fe000 rw-p 00000000 00:00 0 
   2.197 -8a5fe000-8a600000 ---p 00000000 00:00 0 
   2.198 -8a700000-8a7f7000 rw-p 00000000 00:00 0 
   2.199 -8a7f7000-8a800000 ---p 00000000 00:00 0 
   2.200 -8a900000-8a9fc000 rw-p 00000000 00:00 0 
   2.201 -8a9fc000-8aa00000 ---p 00000000 00:00 0 
   2.202 -8ab00000-8abfb000 rw-p 00000000 00:00 0 
   2.203 -8abfb000-8ac00000 ---p 00000000 00:00 0 
   2.204 -8ac00000-8acf5000 rw-p 00000000 00:00 0 
   2.205 -8acf5000-8ad00000 ---p 00000000 00:00 0 
   2.206 -8ad00000-8add3000 rw-p 00000000 00:00 0 
   2.207 -8add3000-8ae00000 ---p 00000000 00:00 0 
   2.208 -8ae00000-8aefb000 rw-p 00000000 00:00 0 
   2.209 -8aefb000-8af00000 ---p 00000000 00:00 0 
   2.210 -8af00000-8afb8000 rw-p 00000000 00:00 0 
   2.211 -8afb8000-8b000000 ---p 00000000 00:00 0 
   2.212 -8b000000-8b0fe000 rw-p 00000000 00:00 0 
   2.213 -8b0fe000-8b100000 ---p 00000000 00:00 0 
   2.214 -8b100000-8b2f9000 rw-p 00000000 00:00 0 
   2.215 -8b2f9000-8b300000 ---p 00000000 00:00 0 
   2.216 -8b300000-8b500000 rw-p 00000000 00:00 0 
   2.217 -8b500000-8b5fd000 rw-p 00000000 00:00 0 
   2.218 -8b5fd000-8b600000 ---p 00000000 00:00 0 
   2.219 -8b600000-8b6ef000 rw-p 00000000 00:00 0 
   2.220 -8b6ef000-8b700000 ---p 00000000 00:00 0 
   2.221 -8b700000-8b7cd000 rw-p 00000000 00:00 0 
   2.222 -8b7cd000-8b800000 ---p 00000000 00:00 0 
   2.223 -8b800000-8b8e7000 rw-p 00000000 00:00 0 
   2.224 -8b8e7000-8b900000 ---p 00000000 00:00 0 
   2.225 -8b900000-8b9fa000 rw-p 00000000 00:00 0 
   2.226 -8b9fa000-8ba00000 ---p 00000000 00:00 0 
   2.227 -8ba27000-8ba3a000 r--s 000b7000 08:05 3147058    /home/gadei/scala/lib/scalap.jar
   2.228 -8ba3a000-8ba48000 r--s 000c5000 08:05 3147104    /home/gadei/scala/lib/scala-swing.jar
   2.229 -8ba48000-8ba50000 r--s 00040000 08:05 3147670    /home/gadei/scala/lib/scala-dbc.jar
   2.230 -8ba50000-8ba52000 r--s 00014000 08:05 3147423    /home/gadei/scala/lib/jline.jar
   2.231 -8ba52000-8baea000 r--s 007ad000 08:05 1976164    /usr/local/jedit_Isac/contrib/jedit-4.3.2/jars/scala-compiler.jar
   2.232 -8baea000-8baf0000 r--s 00061000 08:05 1976160    /usr/local/jedit_Isac/contrib/jedit-4.3.2/jars/Console.jar
   2.233 -8baf0000-8baf5000 r--s 00048000 08:05 1976165    /usr/local/jedit_Isac/contrib/jedit-4.3.2/jars/SideKick.jar
   2.234 -8baf5000-8baf7000 r--s 00003000 08:05 1976159    /usr/local/jedit_Isac/contrib/jedit-4.3.2/jars/Hyperlinks.jar
   2.235 -8baf7000-8baf8000 r--s 0000c000 08:05 1976162    /usr/local/jedit_Isac/contrib/jedit-4.3.2/jars/ErrorList.jar
   2.236 -8baf8000-8bb00000 r--s 000a6000 08:05 1976169    /usr/local/jedit_Isac/contrib/jedit-4.3.2/jars/js.jar
   2.237 -8bb00000-8bbfb000 rw-p 00000000 00:00 0 
   2.238 -8bbfb000-8bc00000 ---p 00000000 00:00 0 
   2.239 -8bc00000-8bc11000 r--s 000c5000 08:05 1976163    /usr/local/jedit_Isac/contrib/jedit-4.3.2/jars/cobra.jar
   2.240 -8bc11000-8bc1e000 r--s 000a1000 08:05 1976158    /usr/local/jedit_Isac/contrib/jedit-4.3.2/jars/Pure.jar
   2.241 -8bc1e000-8bc43000 r--s 0043c000 08:05 2112962    /usr/local/jedit_Isac/src/Tools/isac/jEdit/contrib/jEdit/build/jEdit.jar
   2.242 -8bc43000-8bc46000 r--s 00038000 08:05 1462978    /usr/lib/jvm/java-6-openjdk/jre/lib/ext/sunpkcs11.jar
   2.243 -8bc46000-8bc49000 r--s 00031000 08:05 1462981    /usr/lib/jvm/java-6-openjdk/jre/lib/ext/sunjce_provider.jar
   2.244 -8bc49000-8bc4c000 r--s 00077000 08:05 1462980    /usr/lib/jvm/java-6-openjdk/jre/lib/ext/localedata.jar
   2.245 -8bc4c000-8bc4e000 r--s 00001000 08:05 1462979    /usr/lib/jvm/java-6-openjdk/jre/lib/ext/dnsns.jar
   2.246 -8bc4e000-8bc57000 r--s 000b3000 08:05 1463001    /usr/lib/jvm/java-6-openjdk/jre/lib/rhino.jar
   2.247 -8bc57000-8bc65000 r--s 00351000 08:05 1462970    /usr/lib/jvm/java-6-openjdk/jre/lib/charsets.jar
   2.248 -8bc65000-8bc67000 r--s 00013000 08:05 1462993    /usr/lib/jvm/java-6-openjdk/jre/lib/jce.jar
   2.249 -8bc67000-8bc6d000 r--s 000fc000 08:05 1463000    /usr/lib/jvm/java-6-openjdk/jre/lib/resources.jar
   2.250 -8bc6d000-8bccc000 r--s 00582000 08:05 3147393    /home/gadei/scala/lib/scala-library.jar
   2.251 -8bccc000-8bd64000 r--s 007ae000 08:05 3147710    /home/gadei/scala/lib/scala-compiler.jar
   2.252 -8bd64000-8bd65000 ---p 00000000 00:00 0 
   2.253 -8bd65000-8bde5000 rw-p 00000000 00:00 0 
   2.254 -8bde5000-8bde8000 ---p 00000000 00:00 0 
   2.255 -8bde8000-8be36000 rw-p 00000000 00:00 0 
   2.256 -8be36000-8be39000 ---p 00000000 00:00 0 
   2.257 -8be39000-8beb7000 rw-p 00000000 00:00 0 
   2.258 -8beb7000-8beba000 ---p 00000000 00:00 0 
   2.259 -8beba000-8bf38000 rw-p 00000000 00:00 0 
   2.260 -8bf38000-8bf3b000 ---p 00000000 00:00 0 
   2.261 -8bf3b000-8bf89000 rw-p 00000000 00:00 0 
   2.262 -8bf89000-8bf90000 r--s 00000000 08:05 798417     /usr/lib/gconv/gconv-modules.cache
   2.263 -8bf90000-8bfcf000 r--p 00000000 08:05 794473     /usr/lib/locale/en_US.utf8/LC_CTYPE
   2.264 -8bfcf000-8bfd2000 ---p 00000000 00:00 0 
   2.265 -8bfd2000-8c020000 rw-p 00000000 00:00 0 
   2.266 -8c020000-8c023000 ---p 00000000 00:00 0 
   2.267 -8c023000-8c071000 rw-p 00000000 00:00 0 
   2.268 -8c071000-8c200000 r--s 038bb000 08:05 1447960    /usr/lib/jvm/java-6-openjdk/jre/lib/rt.jar
   2.269 -8c200000-8c2fd000 rw-p 00000000 00:00 0 
   2.270 -8c2fd000-8c300000 ---p 00000000 00:00 0 
   2.271 -8c302000-8c306000 r--s 0007c000 08:05 1462994    /usr/lib/jvm/java-6-openjdk/jre/lib/jsse.jar
   2.272 -8c306000-8c30f000 r--s 00065000 08:05 919509     /usr/share/java/gnome-java-bridge.jar
   2.273 -8c30f000-8c310000 ---p 00000000 00:00 0 
   2.274 -8c310000-8c3c2000 rw-p 00000000 00:00 0 
   2.275 -8c3c2000-8c3c3000 ---p 00000000 00:00 0 
   2.276 -8c3c3000-8c443000 rw-p 00000000 00:00 0 
   2.277 -8c443000-8c444000 ---p 00000000 00:00 0 
   2.278 -8c444000-8c4d6000 rw-p 00000000 00:00 0 
   2.279 -8c4d6000-8c504000 rw-p 00000000 00:00 0 
   2.280 -8c504000-8c516000 rw-p 00000000 00:00 0 
   2.281 -8c516000-8c5af000 rw-p 00000000 00:00 0 
   2.282 -8c5af000-8c5c1000 rw-p 00000000 00:00 0 
   2.283 -8c5c1000-8c5ef000 rw-p 00000000 00:00 0 
   2.284 -8c5ef000-8c601000 rw-p 00000000 00:00 0 
   2.285 -8c601000-8c699000 rw-p 00000000 00:00 0 
   2.286 -8c699000-8c6c8000 rw-p 00000000 00:00 0 
   2.287 -8c6c8000-8c6ef000 rw-p 00000000 00:00 0 
   2.288 -8c6ef000-8e970000 rw-p 00000000 00:00 0 
   2.289 -8e970000-946f0000 rw-p 00000000 00:00 0 
   2.290 -946f0000-96a70000 rw-p 00000000 00:00 0 
   2.291 -96a70000-a9c50000 rw-p 00000000 00:00 0 
   2.292 -a9c50000-af7a0000 rw-p 00000000 00:00 0 
   2.293 -af7a0000-b46f0000 rw-p 00000000 00:00 0 
   2.294 -b46f2000-b46fd000 rw-p 00000000 00:00 0 
   2.295 -b46fd000-b47b2000 rw-p 00000000 00:00 0 
   2.296 -b47b2000-b4a52000 rwxp 00000000 00:00 0 
   2.297 -b4a52000-b77b2000 rw-p 00000000 00:00 0 
   2.298 -b77b2000-b77b5000 ---p 00000000 00:00 0 
   2.299 -b77b5000-b7806000 rw-p 00000000 00:00 0 
   2.300 -b7808000-b780b000 r--s 0000f000 08:05 1462983    /usr/lib/jvm/java-6-openjdk/jre/lib/ext/pulse-java.jar
   2.301 -b780b000-b780d000 r--s 0001d000 08:05 1462999    /usr/lib/jvm/java-6-openjdk/jre/lib/plugin.jar
   2.302 -b780d000-b7812000 r--s 00044000 08:05 1462998    /usr/lib/jvm/java-6-openjdk/jre/lib/netx.jar
   2.303 -b7812000-b781a000 rw-s 00000000 08:05 1448211    /tmp/hsperfdata_gadei/5529
   2.304 -b781a000-b781b000 rw-p 00000000 00:00 0 
   2.305 -b781b000-b781c000 r--p 00000000 00:00 0 
   2.306 -b781c000-b781e000 rw-p 00000000 00:00 0 
   2.307 -bfb5c000-bfb71000 rw-p 00000000 00:00 0          [stack]
   2.308 -
   2.309 -VM Arguments:
   2.310 -java_command: scala.tools.nsc.Main @/tmp/scalac-ant-8019952260520385401.args
   2.311 -Launcher Type: SUN_STANDARD
   2.312 -
   2.313 -Environment Variables:
   2.314 -PATH=/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin:/usr/games
   2.315 -USERNAME=gadei
   2.316 -LD_LIBRARY_PATH=/usr/lib/jvm/java-6-openjdk/jre/lib/i386/server:/usr/lib/jvm/java-6-openjdk/jre/lib/i386:/usr/lib/jvm/java-6-openjdk/jre/../lib/i386:/usr/lib/jvm/java-6-openjdk/jre/lib/i386/client:/usr/lib/jvm/java-6-openjdk/jre/lib/i386:/usr/lib/jvm/java-6-openjdk/jre/../lib/i386
   2.317 -SHELL=/bin/bash
   2.318 -DISPLAY=:0.0
   2.319 -
   2.320 -Signal Handlers:
   2.321 -SIGSEGV: [libjvm.so+0x637540], sa_mask[0]=0x7ffbfeff, sa_flags=0x10000004
   2.322 -SIGBUS: [libjvm.so+0x637540], sa_mask[0]=0x7ffbfeff, sa_flags=0x10000004
   2.323 -SIGFPE: [libjvm.so+0x50e650], sa_mask[0]=0x7ffbfeff, sa_flags=0x10000004
   2.324 -SIGPIPE: [libjvm.so+0x50e650], sa_mask[0]=0x7ffbfeff, sa_flags=0x10000004
   2.325 -SIGXFSZ: [libjvm.so+0x50e650], sa_mask[0]=0x7ffbfeff, sa_flags=0x10000004
   2.326 -SIGILL: [libjvm.so+0x50e650], sa_mask[0]=0x7ffbfeff, sa_flags=0x10000004
   2.327 -SIGUSR1: SIG_DFL, sa_mask[0]=0x00000000, sa_flags=0x00000000
   2.328 -SIGUSR2: [libjvm.so+0x50dd00], sa_mask[0]=0x00000004, sa_flags=0x10000004
   2.329 -SIGHUP: [libjvm.so+0x510870], sa_mask[0]=0x7ffbfeff, sa_flags=0x10000004
   2.330 -SIGINT: SIG_IGN, sa_mask[0]=0x00000000, sa_flags=0x00000000
   2.331 -SIGTERM: [libjvm.so+0x510870], sa_mask[0]=0x7ffbfeff, sa_flags=0x10000004
   2.332 -SIGQUIT: [libjvm.so+0x510870], sa_mask[0]=0x7ffbfeff, sa_flags=0x10000004
   2.333 -
   2.334 -
   2.335 ----------------  S Y S T E M  ---------------
   2.336 -
   2.337 -OS:Ubuntu 10.04 (lucid)
   2.338 -uname:Linux 2.6.32-28-generic #55-Ubuntu SMP Mon Jan 10 21:21:01 UTC 2011 i686
   2.339 -libc:glibc 2.11.1 NPTL 2.11.1 
   2.340 -rlimit: STACK 8192k, CORE 0k, NPROC infinity, NOFILE 1024, AS infinity
   2.341 -load average:1.12 0.69 0.64
   2.342 -
   2.343 -/proc/meminfo:
   2.344 -MemTotal:        2027000 kB
   2.345 -MemFree:           71488 kB
   2.346 -Buffers:          114588 kB
   2.347 -Cached:          1036544 kB
   2.348 -SwapCached:            0 kB
   2.349 -Active:          1184100 kB
   2.350 -Inactive:         629644 kB
   2.351 -Active(anon):     610028 kB
   2.352 -Inactive(anon):   112804 kB
   2.353 -Active(file):     574072 kB
   2.354 -Inactive(file):   516840 kB
   2.355 -Unevictable:           0 kB
   2.356 -Mlocked:               0 kB
   2.357 -HighTotal:       1152712 kB
   2.358 -HighFree:           1736 kB
   2.359 -LowTotal:         874288 kB
   2.360 -LowFree:           69752 kB
   2.361 -SwapTotal:       4288504 kB
   2.362 -SwapFree:        4288504 kB
   2.363 -Dirty:                92 kB
   2.364 -Writeback:             0 kB
   2.365 -AnonPages:        662552 kB
   2.366 -Mapped:           122776 kB
   2.367 -Shmem:             60220 kB
   2.368 -Slab:              82612 kB
   2.369 -SReclaimable:      67088 kB
   2.370 -SUnreclaim:        15524 kB
   2.371 -KernelStack:        2632 kB
   2.372 -PageTables:         6552 kB
   2.373 -NFS_Unstable:          0 kB
   2.374 -Bounce:                0 kB
   2.375 -WritebackTmp:          0 kB
   2.376 -CommitLimit:     5302004 kB
   2.377 -Committed_AS:    1524016 kB
   2.378 -VmallocTotal:     122880 kB
   2.379 -VmallocUsed:       38656 kB
   2.380 -VmallocChunk:      58164 kB
   2.381 -HardwareCorrupted:     0 kB
   2.382 -HugePages_Total:       0
   2.383 -HugePages_Free:        0
   2.384 -HugePages_Rsvd:        0
   2.385 -HugePages_Surp:        0
   2.386 -Hugepagesize:       4096 kB
   2.387 -DirectMap4k:       16376 kB
   2.388 -DirectMap4M:      892928 kB
   2.389 -
   2.390 -
   2.391 -CPU:total 2 (2 cores per cpu, 1 threads per core) family 6 model 15 stepping 13, cmov, cx8, fxsr, mmx, sse, sse2, sse3, ssse3
   2.392 -
   2.393 -Memory: 4k page, physical 2027000k(71488k free), swap 4288504k(4288504k free)
   2.394 -
   2.395 -vm_info: OpenJDK Server VM (19.0-b09) for linux-x86 JRE (1.6.0_20-b20), built on Jan  7 2011 19:33:58 by "buildd" with gcc 4.4.3
   2.396 -
   2.397 -time: Fri Jan 28 16:56:05 2011
   2.398 -elapsed time: 10 seconds
   2.399 -

     3.1 --- a/test/Tools/isac/Frontend/interface.sml	Sat Jun 18 11:28:10 2011 +0200
     3.2 +++ b/test/Tools/isac/Frontend/interface.sml	Mon Jun 20 17:33:06 2011 +0200
     3.3 @@ -140,6 +140,7 @@
     3.4   val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
     3.5  
     3.6   setNextTactic 1 (Apply_Method ["Test","solve_linear"]);
     3.7 +   (*ERROR.110620 <SETNEXTTACTIC>..<MESSAGE> end-of-calculation*)
     3.8   val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
     3.9   is_complete_mod ptp;
    3.10   is_complete_spec ptp;
    3.11 @@ -167,8 +168,9 @@
    3.12       (*exception just above means: 'ModSpec' has been returned: error anyway*)
    3.13   if term2str f = "[x = 1]" then () else 
    3.14   error "FE-Kernel-interface.sml: diff.behav. in solve_linear as rootpbl";
    3.15 +============ inhibit exn 110310 ==============================================*)
    3.16  
    3.17 -
    3.18 +(*========== inhibit exn 110620 ================================================
    3.19  "--------- inspect the CalcTree No.1 with Iterator No.2 -";
    3.20  "--------- inspect the CalcTree No.1 with Iterator No.2 -";
    3.21  "--------- inspect the CalcTree No.1 with Iterator No.2 -";
    3.22 @@ -191,7 +193,7 @@
    3.23   if get_pos 1 1 = ([], Res) then () else 
    3.24   error "FE-interface.sml: diff.behav. in b inspect 1 with Iterator 2";
    3.25   moveActiveCalcHead 1; refFormula 1 ([],Pbl);
    3.26 -
    3.27 +============ inhibit exn 110620 ==============================================*)
    3.28  
    3.29  "--------- miniscript with mini-subpbl ------------------";
    3.30  "--------- miniscript with mini-subpbl ------------------";
    3.31 @@ -316,7 +318,6 @@
    3.32  
    3.33   DEconstrCalcTree 1;
    3.34  
    3.35 -
    3.36  "--------- mini-subpbl AUTOCALCULATE Step 1 -------------";
    3.37  "--------- mini-subpbl AUTOCALCULATE Step 1 -------------";
    3.38  "--------- mini-subpbl AUTOCALCULATE Step 1 -------------";
    3.39 @@ -369,6 +370,7 @@
    3.40  
    3.41   DEconstrCalcTree 1;
    3.42  
    3.43 +(*========== inhibit exn 110620 ================================================
    3.44  "--------- solve_linear as rootpbl AUTO CompleteCalc ----";
    3.45  "--------- solve_linear as rootpbl AUTO CompleteCalc ----";
    3.46  "--------- solve_linear as rootpbl AUTO CompleteCalc ----";
    3.47 @@ -392,7 +394,6 @@
    3.48   if term2str f = "[x = 1]" andalso p = ([], Res) then () else 
    3.49   error "FE-interface.sml: diff.behav. in solve_linear/rt AUTOCALCULATE ";
    3.50  
    3.51 -
    3.52  "--------- solve_linear as rootpbl AUTO CompleteHead/Calc ";
    3.53  "--------- solve_linear as rootpbl AUTO CompleteHead/Calc ";
    3.54  "--------- solve_linear as rootpbl AUTO CompleteHead/Calc ";
    3.55 @@ -408,13 +409,11 @@
    3.56   refFormula 1 (get_pos 1 1);
    3.57   val ((pt,p),_) = get_calc 1;
    3.58  
    3.59 -
    3.60 -
    3.61   autoCalculate 1 CompleteCalc; 
    3.62   val ((pt,p),_) = get_calc 1;
    3.63   if p=([], Res) then () else 
    3.64   error "FE-interface.sml: diff.behav. in solve_linear AUTOC Head/Calc ";
    3.65 -
    3.66 +============ inhibit exn 110620 ==============================================*)
    3.67  
    3.68  "--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";
    3.69  "--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";
    3.70 @@ -441,11 +440,15 @@
    3.71  
    3.72   val ((pt,_),_) = get_calc 1;
    3.73   val p = get_pos 1 1;
    3.74 +(*========== inhibit exn 110620 ================================================
    3.75   val (Form f, tac, asms) = pt_extract (pt, p);
    3.76 +(*    ModSpec........... =  ...................DIFFERENT !*)
    3.77   if term2str f = "[x = 1]" andalso p = ([], Res) then () else 
    3.78   error "FE-interface.sml: diff.behav. in mini-subpbl AUTOCALCULATE 6";
    3.79 +============ inhibit exn 110620 ==============================================*)
    3.80  
    3.81  
    3.82 +(*=== inhibit exn ?=============================================================
    3.83  "--------- mini-subpbl AUTO CompleteCalcHead ------------";
    3.84  "--------- mini-subpbl AUTO CompleteCalcHead ------------";
    3.85  "--------- mini-subpbl AUTO CompleteCalcHead ------------";
    3.86 @@ -454,6 +457,7 @@
    3.87     ("Test", ["sqroot-test","univariate","equation","test"],
    3.88      ["Test","squ-equ-test-subpbl1"]))];
    3.89   Iterator 1;
    3.90 + moveActiveRoot 1;
    3.91  (* doesn't terminate !!!
    3.92   autoCalculate 1 CompleteCalcHead; 
    3.93  *)
    3.94 @@ -1314,4 +1318,5 @@
    3.95   if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else 
    3.96   error "FE-interface.sml: diff.behav. in FORMULA:replace} NOTok";
    3.97  
    3.98 -============ inhibit exn 110310 ==============================================*)
    3.99 +===== inhibit exn ?===========================================================*)
   3.100 +

     4.1 --- a/test/Tools/isac/Test_Isac.thy	Sat Jun 18 11:28:10 2011 +0200
     4.2 +++ b/test/Tools/isac/Test_Isac.thy	Mon Jun 20 17:33:06 2011 +0200
     4.3 @@ -12,7 +12,15 @@
     4.4    Isac
     4.5    "Knowledge/Rational_Test"
     4.6    "ADDTESTS/Ctxt"
     4.7 +  "ADDTESTS/test-depend/Build_Test"
     4.8    "ADDTESTS/All_Ctxt"
     4.9 +(*"ADDTESTS/course/T2_Rewriting" theory has not been declared*)
    4.10 +(*"ADDTESTS/course/T1_Basics.thy" could not find ^^^*)
    4.11 +(*"ADDTESTS/course/T3_MathEngine" could not find ^^^*)
    4.12 +  "ADDTESTS/file-depend/Build_Test"
    4.13 +  "../../Pure/Isar/Test_Parsers"
    4.14 +(*"../../Pure/Isar/Pure/Isar/Struct_Deriv" update 2009-2-->2011*)
    4.15 +  "../../Pure/Isar/Test_Parse_Term"
    4.16   
    4.17  uses 
    4.18    (         "library.sml")
    4.19 @@ -131,7 +139,23 @@
    4.20    ML {*"%%%%%%%%%%%%%%%%% start Frontend.thy %%%%%%%%%%%%%%%%%%%";*}
    4.21    use "Frontend/messages.sml"        (*new 2011*)
    4.22    use "Frontend/states.sml"          (*new 2011*)
    4.23 -  use "Frontend/interface.sml"       (*part.*)                            
    4.24 +  use "Frontend/interface.sml"       (*part.*)
    4.25 +ML {*
    4.26 +
    4.27 +*}
    4.28 +ML {*
    4.29 +
    4.30 +*}
    4.31 +ML {*
    4.32 +
    4.33 +*}
    4.34 +ML {*
    4.35 +
    4.36 +*}
    4.37 +ML {*
    4.38 +
    4.39 +*}
    4.40 +                            
    4.41    use         "print_exn_G.sml"      (*new 2011*)
    4.42    ML {*"%%%%%%%%%%%%%%%%% end Frontend.thy %%%%%%%%%%%%%%%%%%%%%";*}
    4.43    ML {*"%%%%%%%%%%%%%%%%% start Knowledge.thy %%%%%%%%%%%%%%%%%%";*}
    4.44 @@ -171,11 +195,16 @@
    4.45    ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*}
    4.46  
    4.47  ML {*
    4.48 -*}
    4.49 -ML {*
    4.50 -*}
    4.51 -  ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*}
    4.52 -ML {*
    4.53 +"--------- mini-subpbl AUTO CompleteCalcHead ------------";
    4.54 + states:=[];
    4.55 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], 
    4.56 +   ("Test", ["sqroot-test","univariate","equation","test"],
    4.57 +    ["Test","squ-equ-test-subpbl1"]))];
    4.58 + Iterator 1;
    4.59 + moveActiveRoot 1;
    4.60 +(* doesn't terminate !!!*)
    4.61 + autoCalculate 1 CompleteCalcHead; 
    4.62 +val (ModSpec (x1,x2,x3,x4,x5,x6), tac, asms) =  pt_extract (pt, p);
    4.63  *}
    4.64  ML {*
    4.65  *}
    4.66 @@ -183,20 +212,19 @@
    4.67  *}
    4.68  ML {*
    4.69  *}
    4.70 -ML {*
    4.71 -*}
    4.72 +  ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*}
    4.73  
    4.74  end
    4.75  
    4.76  (*=== inhibit exn ?=============================================================
    4.77  ===== inhibit exn ?===========================================================*)
    4.78  
    4.79 -(*========== inhibit exn 110520 ================================================
    4.80 +(*========== inhibit exn 110620 ================================================
    4.81  
    4.82  "########### testcode inserted vvv ###########################################";
    4.83  "########### testcode inserted ^^^ ###########################################";
    4.84  
    4.85 -============ inhibit exn 110520 ==============================================*)
    4.86 +============ inhibit exn 110620 ==============================================*)
    4.87  
    4.88  (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
    4.89  -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)