# HG changeset patch # User Walther Neuper # Date 1308583986 -7200 # Node ID 6548da70f14e7bfbc4895b6056b5595ea82742ec # Parent f6a001b47a84ffc228720b7ce12c0762d82cab1f intermed: bakk msteger 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} diff -r f6a001b47a84 -r 6548da70f14e src/Tools/jEditC/hs_err_pid5529.log --- a/src/Tools/jEditC/hs_err_pid5529.log Sat Jun 18 11:28:10 2011 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,396 +0,0 @@ -# -# A fatal error has been detected by the Java Runtime Environment: -# -# SIGSEGV (0xb) at pc=0xb499496b, pid=5529, tid=3078630256 -# -# JRE version: 6.0_20-b20 -# Java VM: OpenJDK Server VM (19.0-b09 mixed mode linux-x86 ) -# Derivative: IcedTea6 1.9.4 -# Distribution: Ubuntu 10.04.1 LTS, package 6b20-1.9.4-0ubuntu1~10.04.1 -# Problematic frame: -# J scala.tools.nsc.transform.UnCurry$$anon$3.apply(Lscala/tools/nsc/symtab/Types$Type;)Lscala/tools/nsc/symtab/Types$Type; -# -# If you would like to submit a bug report, please include -# instructions how to reproduce the bug and visit: -# https://bugs.launchpad.net/ubuntu/+source/openjdk-6/ -# - ---------------- T H R E A D --------------- - -Current thread (0x0813e400): JavaThread "main" [_thread_in_Java, id=5532, stack(0xb77b2000,0xb7803000)] - -siginfo:si_signo=SIGSEGV: si_errno=0, si_code=128 (), si_addr=0x00000000 - -Registers: -EAX=0x95763760, EBX=0x955105b8, ECX=0x9586cf98, EDX=0x95763760 -ESP=0xb7800f10, EBP=0x9586cf58, ESI=0xb7800f6c, EDI=0x9586cf58 -EIP=0xb499496b, CR2=0x00000008, EFLAGS=0x00210206 - -Register to memory mapping: - -EAX=0x95763760 -scala.tools.nsc.symtab.Types$TypeRef$rawTypeRef$1 - - klass: 'scala/tools/nsc/symtab/Types$TypeRef$rawTypeRef$1' - -EBX=0x955105b8 -scala.tools.nsc.symtab.Symbols$ClassSymbol - - klass: 'scala/tools/nsc/symtab/Symbols$ClassSymbol' - -ECX=0x9586cf98 -scala.tools.nsc.transform.UnCurry$$anon$3 - - klass: 'scala/tools/nsc/transform/UnCurry$$anon$3' - -EDX=0x95763760 -scala.tools.nsc.symtab.Types$TypeRef$rawTypeRef$1 - - klass: 'scala/tools/nsc/symtab/Types$TypeRef$rawTypeRef$1' - -ESP=0xb7800f10 -0xb7800f10 is pointing into the stack for thread: 0x0813e400 -"main" prio=10 tid=0x0813e400 nid=0x159c runnable [0x00000000] - java.lang.Thread.State: RUNNABLE - -EBP=0x9586cf58 -scala.tools.nsc.Global$uncurry$ - - klass: 'scala/tools/nsc/Global$uncurry$' - -ESI=0xb7800f6c -0xb7800f6c is pointing into the stack for thread: 0x0813e400 -"main" prio=10 tid=0x0813e400 nid=0x159c runnable [0x00000000] - java.lang.Thread.State: RUNNABLE - -EDI=0x9586cf58 -scala.tools.nsc.Global$uncurry$ - - klass: 'scala/tools/nsc/Global$uncurry$' - - -Top of Stack: (sp=0xb7800f10) -0xb7800f10: 948dd5f8 955d5430 9586cf98 9586cf58 -0xb7800f20: 9480b4a0 957637a8 948e21c8 95b761e8 -0xb7800f30: 95763760 95b761e8 00b6e39f 0813e400 -0xb7800f40: 8c2f8818 b7800f74 8ce92f40 b480aaf0 -0xb7800f50: b7800f70 8d0aa7a0 b7800f94 b47b5523 -0xb7800f60: 00000000 b7800f70 b47b5523 95763760 -0xb7800f70: 9586cf98 b7800f74 8d65624f b7800fa8 -0xb7800f80: 8d6568d8 8d820a68 8d6562b0 b7800f6c - -Instructions: (pc=0xb499496b) -0xb499495b: 8c 0f 84 9b 09 00 00 8b 4c 24 08 8b 54 24 20 90 -0xb499496b: e8 5c 27 0a 00 89 44 24 08 85 ed 0f 84 71 09 00 - -Stack: [0xb77b2000,0xb7803000], sp=0xb7800f10, free space=315k -Native frames: (J=compiled Java code, j=interpreted, Vv=VM code, C=native code) -J scala.tools.nsc.transform.UnCurry$$anon$3.apply(Lscala/tools/nsc/symtab/Types$Type;)Lscala/tools/nsc/symtab/Types$Type; - - ---------------- P R O C E S S --------------- - -Java Threads: ( => current thread ) - 0x8c296800 JavaThread "Low Memory Detector" daemon [_thread_blocked, id=5541, stack(0x8bde5000,0x8be36000)] - 0x8c294c00 JavaThread "CompilerThread1" daemon [_thread_in_native, id=5540, stack(0x8be36000,0x8beb7000)] - 0x8c292800 JavaThread "CompilerThread0" daemon [_thread_in_native, id=5539, stack(0x8beb7000,0x8bf38000)] - 0x8c291000 JavaThread "Signal Dispatcher" daemon [_thread_blocked, id=5538, stack(0x8bf38000,0x8bf89000)] - 0x8c281000 JavaThread "Finalizer" daemon [_thread_blocked, id=5537, stack(0x8bfcf000,0x8c020000)] - 0x8c27f800 JavaThread "Reference Handler" daemon [_thread_blocked, id=5536, stack(0x8c020000,0x8c071000)] -=>0x0813e400 JavaThread "main" [_thread_in_Java, id=5532, stack(0xb77b2000,0xb7803000)] - -Other Threads: - 0x8c27bc00 VMThread [stack: 0x8c30f000,0x8c390000] [id=5535] - 0x8c298c00 WatcherThread [stack: 0x8bd64000,0x8bde5000] [id=5542] - -VM state:not at safepoint (normal execution) - -VM Mutex/Monitor currently owned by a thread: None - -Heap - PSYoungGen total 84864K, used 34429K [0xa9c50000, 0xaf7a0000, 0xb46f0000) - eden space 76224K, 45% used [0xa9c50000,0xabdef708,0xae6c0000) - from space 8640K, 0% used [0xaef30000,0xaef30000,0xaf7a0000) - to space 8640K, 0% used [0xae6c0000,0xae6c0000,0xaef30000) - PSOldGen total 36352K, used 21119K [0x946f0000, 0x96a70000, 0xa9c50000) - object space 36352K, 58% used [0x946f0000,0x95b8ffe8,0x96a70000) - PSPermGen total 35328K, used 19196K [0x8c6f0000, 0x8e970000, 0x946f0000) - object space 35328K, 54% used [0x8c6f0000,0x8d9af0a0,0x8e970000) - -Dynamic libraries: -00110000-00117000 r-xp 00000000 08:05 2367999 /lib/tls/i686/cmov/librt-2.11.1.so -00117000-00118000 r--p 00006000 08:05 2367999 /lib/tls/i686/cmov/librt-2.11.1.so -00118000-00119000 rw-p 00007000 08:05 2367999 /lib/tls/i686/cmov/librt-2.11.1.so -00119000-00123000 r-xp 00000000 08:05 2367987 /lib/tls/i686/cmov/libnss_files-2.11.1.so -00123000-00124000 r--p 00009000 08:05 2367987 /lib/tls/i686/cmov/libnss_files-2.11.1.so -00124000-00125000 rw-p 0000a000 08:05 2367987 /lib/tls/i686/cmov/libnss_files-2.11.1.so -00163000-00187000 r-xp 00000000 08:05 2367994 /lib/tls/i686/cmov/libm-2.11.1.so -00187000-00188000 r--p 00023000 08:05 2367994 /lib/tls/i686/cmov/libm-2.11.1.so -00188000-00189000 rw-p 00024000 08:05 2367994 /lib/tls/i686/cmov/libm-2.11.1.so -00189000-0019d000 r-xp 00000000 08:05 1447999 /usr/lib/jvm/java-6-openjdk/jre/lib/i386/libnet.so -0019d000-0019e000 r--p 00013000 08:05 1447999 /usr/lib/jvm/java-6-openjdk/jre/lib/i386/libnet.so -0019e000-0019f000 rw-p 00014000 08:05 1447999 /usr/lib/jvm/java-6-openjdk/jre/lib/i386/libnet.so -0021a000-0023e000 r-xp 00000000 08:05 1447986 /usr/lib/jvm/java-6-openjdk/jre/lib/i386/libjava.so -0023e000-0023f000 r--p 00023000 08:05 1447986 /usr/lib/jvm/java-6-openjdk/jre/lib/i386/libjava.so -0023f000-00241000 rw-p 00024000 08:05 1447986 /usr/lib/jvm/java-6-openjdk/jre/lib/i386/libjava.so -00286000-0028c000 r-xp 00000000 08:05 2368006 /lib/tls/i686/cmov/libnss_compat-2.11.1.so -0028c000-0028d000 r--p 00006000 08:05 2368006 /lib/tls/i686/cmov/libnss_compat-2.11.1.so -0028d000-0028e000 rw-p 00007000 08:05 2368006 /lib/tls/i686/cmov/libnss_compat-2.11.1.so -00534000-00687000 r-xp 00000000 08:05 2367991 /lib/tls/i686/cmov/libc-2.11.1.so -00687000-00688000 ---p 00153000 08:05 2367991 /lib/tls/i686/cmov/libc-2.11.1.so -00688000-0068a000 r--p 00153000 08:05 2367991 /lib/tls/i686/cmov/libc-2.11.1.so -0068a000-0068b000 rw-p 00155000 08:05 2367991 /lib/tls/i686/cmov/libc-2.11.1.so -0068b000-0068e000 rw-p 00000000 00:00 0 -0081c000-0081f000 r-xp 00000000 08:05 1447967 /usr/lib/jvm/java-6-openjdk/jre/lib/i386/jli/libjli.so -0081f000-00820000 r--p 00003000 08:05 1447967 /usr/lib/jvm/java-6-openjdk/jre/lib/i386/jli/libjli.so -00820000-00821000 rw-p 00004000 08:05 1447967 /usr/lib/jvm/java-6-openjdk/jre/lib/i386/jli/libjli.so -00944000-0094b000 r-xp 00000000 08:05 1448000 /usr/lib/jvm/java-6-openjdk/jre/lib/i386/libnio.so -0094b000-0094c000 r--p 00006000 08:05 1448000 /usr/lib/jvm/java-6-openjdk/jre/lib/i386/libnio.so -0094c000-0094d000 rw-p 00007000 08:05 1448000 /usr/lib/jvm/java-6-openjdk/jre/lib/i386/libnio.so -00a35000-00a3c000 r-xp 00000000 08:05 1448009 /usr/lib/jvm/java-6-openjdk/jre/lib/i386/libzip.so -00a3c000-00a3d000 r--p 00006000 08:05 1448009 /usr/lib/jvm/java-6-openjdk/jre/lib/i386/libzip.so -00a3d000-00a3e000 rw-p 00007000 08:05 1448009 /usr/lib/jvm/java-6-openjdk/jre/lib/i386/libzip.so -00a8f000-00a96000 r-xp 00000000 08:05 1448010 /usr/lib/jvm/java-6-openjdk/jre/lib/i386/native_threads/libhpi.so -00a96000-00a97000 r--p 00006000 08:05 1448010 /usr/lib/jvm/java-6-openjdk/jre/lib/i386/native_threads/libhpi.so -00a97000-00a98000 rw-p 00007000 08:05 1448010 /usr/lib/jvm/java-6-openjdk/jre/lib/i386/native_threads/libhpi.so -00acb000-00acd000 r-xp 00000000 08:05 2367985 /lib/tls/i686/cmov/libdl-2.11.1.so -00acd000-00ace000 r--p 00001000 08:05 2367985 /lib/tls/i686/cmov/libdl-2.11.1.so -00ace000-00acf000 rw-p 00002000 08:05 2367985 /lib/tls/i686/cmov/libdl-2.11.1.so -00b01000-00b02000 r-xp 00000000 00:00 0 [vdso] -00b26000-00b32000 r-xp 00000000 08:05 1448008 /usr/lib/jvm/java-6-openjdk/jre/lib/i386/libverify.so -00b32000-00b33000 r--p 0000b000 08:05 1448008 /usr/lib/jvm/java-6-openjdk/jre/lib/i386/libverify.so -00b33000-00b34000 rw-p 0000c000 08:05 1448008 /usr/lib/jvm/java-6-openjdk/jre/lib/i386/libverify.so -00cad000-00cc2000 r-xp 00000000 08:05 2367986 /lib/tls/i686/cmov/libpthread-2.11.1.so -00cc2000-00cc3000 r--p 00014000 08:05 2367986 /lib/tls/i686/cmov/libpthread-2.11.1.so -00cc3000-00cc4000 rw-p 00015000 08:05 2367986 /lib/tls/i686/cmov/libpthread-2.11.1.so -00cc4000-00cc6000 rw-p 00000000 00:00 0 -00d40000-00d53000 r-xp 00000000 08:05 2359494 /lib/libz.so.1.2.3.3 -00d53000-00d54000 r--p 00012000 08:05 2359494 /lib/libz.so.1.2.3.3 -00d54000-00d55000 rw-p 00013000 08:05 2359494 /lib/libz.so.1.2.3.3 -00e0e000-00e16000 r-xp 00000000 08:05 2368007 /lib/tls/i686/cmov/libnss_nis-2.11.1.so -00e16000-00e17000 r--p 00007000 08:05 2368007 /lib/tls/i686/cmov/libnss_nis-2.11.1.so -00e17000-00e18000 rw-p 00008000 08:05 2368007 /lib/tls/i686/cmov/libnss_nis-2.11.1.so -00ebc000-00ecf000 r-xp 00000000 08:05 2359410 /lib/tls/i686/cmov/libnsl-2.11.1.so -00ecf000-00ed0000 r--p 00012000 08:05 2359410 /lib/tls/i686/cmov/libnsl-2.11.1.so -00ed0000-00ed1000 rw-p 00013000 08:05 2359410 /lib/tls/i686/cmov/libnsl-2.11.1.so -00ed1000-00ed3000 rw-p 00000000 00:00 0 -00fe0000-00ffb000 r-xp 00000000 08:05 2359672 /lib/ld-2.11.1.so -00ffb000-00ffc000 r--p 0001a000 08:05 2359672 /lib/ld-2.11.1.so -00ffc000-00ffd000 rw-p 0001b000 08:05 2359672 /lib/ld-2.11.1.so -00ffd000-016af000 r-xp 00000000 08:05 1448011 /usr/lib/jvm/java-6-openjdk/jre/lib/i386/server/libjvm.so -016af000-016b0000 ---p 006b2000 08:05 1448011 /usr/lib/jvm/java-6-openjdk/jre/lib/i386/server/libjvm.so -016b0000-016f5000 r--p 006b2000 08:05 1448011 /usr/lib/jvm/java-6-openjdk/jre/lib/i386/server/libjvm.so -016f5000-01704000 rw-p 006f7000 08:05 1448011 /usr/lib/jvm/java-6-openjdk/jre/lib/i386/server/libjvm.so -01704000-01b23000 rw-p 00000000 00:00 0 -08048000-08051000 r-xp 00000000 08:05 1463022 /usr/lib/jvm/java-6-openjdk/jre/bin/java -08051000-08052000 r--p 00008000 08:05 1463022 /usr/lib/jvm/java-6-openjdk/jre/bin/java -08052000-08053000 rw-p 00009000 08:05 1463022 /usr/lib/jvm/java-6-openjdk/jre/bin/java -08138000-08ec2000 rw-p 00000000 00:00 0 [heap] -89d00000-89df9000 rw-p 00000000 00:00 0 -89df9000-89e00000 ---p 00000000 00:00 0 -89f00000-89ffb000 rw-p 00000000 00:00 0 -89ffb000-8a000000 ---p 00000000 00:00 0 -8a100000-8a17f000 rw-p 00000000 00:00 0 -8a17f000-8a200000 ---p 00000000 00:00 0 -8a300000-8a3f5000 rw-p 00000000 00:00 0 -8a3f5000-8a400000 ---p 00000000 00:00 0 -8a400000-8a4f8000 rw-p 00000000 00:00 0 -8a4f8000-8a500000 ---p 00000000 00:00 0 -8a500000-8a5fe000 rw-p 00000000 00:00 0 -8a5fe000-8a600000 ---p 00000000 00:00 0 -8a700000-8a7f7000 rw-p 00000000 00:00 0 -8a7f7000-8a800000 ---p 00000000 00:00 0 -8a900000-8a9fc000 rw-p 00000000 00:00 0 -8a9fc000-8aa00000 ---p 00000000 00:00 0 -8ab00000-8abfb000 rw-p 00000000 00:00 0 -8abfb000-8ac00000 ---p 00000000 00:00 0 -8ac00000-8acf5000 rw-p 00000000 00:00 0 -8acf5000-8ad00000 ---p 00000000 00:00 0 -8ad00000-8add3000 rw-p 00000000 00:00 0 -8add3000-8ae00000 ---p 00000000 00:00 0 -8ae00000-8aefb000 rw-p 00000000 00:00 0 -8aefb000-8af00000 ---p 00000000 00:00 0 -8af00000-8afb8000 rw-p 00000000 00:00 0 -8afb8000-8b000000 ---p 00000000 00:00 0 -8b000000-8b0fe000 rw-p 00000000 00:00 0 -8b0fe000-8b100000 ---p 00000000 00:00 0 -8b100000-8b2f9000 rw-p 00000000 00:00 0 -8b2f9000-8b300000 ---p 00000000 00:00 0 -8b300000-8b500000 rw-p 00000000 00:00 0 -8b500000-8b5fd000 rw-p 00000000 00:00 0 -8b5fd000-8b600000 ---p 00000000 00:00 0 -8b600000-8b6ef000 rw-p 00000000 00:00 0 -8b6ef000-8b700000 ---p 00000000 00:00 0 -8b700000-8b7cd000 rw-p 00000000 00:00 0 -8b7cd000-8b800000 ---p 00000000 00:00 0 -8b800000-8b8e7000 rw-p 00000000 00:00 0 -8b8e7000-8b900000 ---p 00000000 00:00 0 -8b900000-8b9fa000 rw-p 00000000 00:00 0 -8b9fa000-8ba00000 ---p 00000000 00:00 0 -8ba27000-8ba3a000 r--s 000b7000 08:05 3147058 /home/gadei/scala/lib/scalap.jar -8ba3a000-8ba48000 r--s 000c5000 08:05 3147104 /home/gadei/scala/lib/scala-swing.jar -8ba48000-8ba50000 r--s 00040000 08:05 3147670 /home/gadei/scala/lib/scala-dbc.jar -8ba50000-8ba52000 r--s 00014000 08:05 3147423 /home/gadei/scala/lib/jline.jar -8ba52000-8baea000 r--s 007ad000 08:05 1976164 /usr/local/jedit_Isac/contrib/jedit-4.3.2/jars/scala-compiler.jar -8baea000-8baf0000 r--s 00061000 08:05 1976160 /usr/local/jedit_Isac/contrib/jedit-4.3.2/jars/Console.jar -8baf0000-8baf5000 r--s 00048000 08:05 1976165 /usr/local/jedit_Isac/contrib/jedit-4.3.2/jars/SideKick.jar -8baf5000-8baf7000 r--s 00003000 08:05 1976159 /usr/local/jedit_Isac/contrib/jedit-4.3.2/jars/Hyperlinks.jar -8baf7000-8baf8000 r--s 0000c000 08:05 1976162 /usr/local/jedit_Isac/contrib/jedit-4.3.2/jars/ErrorList.jar -8baf8000-8bb00000 r--s 000a6000 08:05 1976169 /usr/local/jedit_Isac/contrib/jedit-4.3.2/jars/js.jar -8bb00000-8bbfb000 rw-p 00000000 00:00 0 -8bbfb000-8bc00000 ---p 00000000 00:00 0 -8bc00000-8bc11000 r--s 000c5000 08:05 1976163 /usr/local/jedit_Isac/contrib/jedit-4.3.2/jars/cobra.jar -8bc11000-8bc1e000 r--s 000a1000 08:05 1976158 /usr/local/jedit_Isac/contrib/jedit-4.3.2/jars/Pure.jar -8bc1e000-8bc43000 r--s 0043c000 08:05 2112962 /usr/local/jedit_Isac/src/Tools/isac/jEdit/contrib/jEdit/build/jEdit.jar -8bc43000-8bc46000 r--s 00038000 08:05 1462978 /usr/lib/jvm/java-6-openjdk/jre/lib/ext/sunpkcs11.jar -8bc46000-8bc49000 r--s 00031000 08:05 1462981 /usr/lib/jvm/java-6-openjdk/jre/lib/ext/sunjce_provider.jar -8bc49000-8bc4c000 r--s 00077000 08:05 1462980 /usr/lib/jvm/java-6-openjdk/jre/lib/ext/localedata.jar -8bc4c000-8bc4e000 r--s 00001000 08:05 1462979 /usr/lib/jvm/java-6-openjdk/jre/lib/ext/dnsns.jar -8bc4e000-8bc57000 r--s 000b3000 08:05 1463001 /usr/lib/jvm/java-6-openjdk/jre/lib/rhino.jar -8bc57000-8bc65000 r--s 00351000 08:05 1462970 /usr/lib/jvm/java-6-openjdk/jre/lib/charsets.jar -8bc65000-8bc67000 r--s 00013000 08:05 1462993 /usr/lib/jvm/java-6-openjdk/jre/lib/jce.jar -8bc67000-8bc6d000 r--s 000fc000 08:05 1463000 /usr/lib/jvm/java-6-openjdk/jre/lib/resources.jar -8bc6d000-8bccc000 r--s 00582000 08:05 3147393 /home/gadei/scala/lib/scala-library.jar -8bccc000-8bd64000 r--s 007ae000 08:05 3147710 /home/gadei/scala/lib/scala-compiler.jar -8bd64000-8bd65000 ---p 00000000 00:00 0 -8bd65000-8bde5000 rw-p 00000000 00:00 0 -8bde5000-8bde8000 ---p 00000000 00:00 0 -8bde8000-8be36000 rw-p 00000000 00:00 0 -8be36000-8be39000 ---p 00000000 00:00 0 -8be39000-8beb7000 rw-p 00000000 00:00 0 -8beb7000-8beba000 ---p 00000000 00:00 0 -8beba000-8bf38000 rw-p 00000000 00:00 0 -8bf38000-8bf3b000 ---p 00000000 00:00 0 -8bf3b000-8bf89000 rw-p 00000000 00:00 0 -8bf89000-8bf90000 r--s 00000000 08:05 798417 /usr/lib/gconv/gconv-modules.cache -8bf90000-8bfcf000 r--p 00000000 08:05 794473 /usr/lib/locale/en_US.utf8/LC_CTYPE -8bfcf000-8bfd2000 ---p 00000000 00:00 0 -8bfd2000-8c020000 rw-p 00000000 00:00 0 -8c020000-8c023000 ---p 00000000 00:00 0 -8c023000-8c071000 rw-p 00000000 00:00 0 -8c071000-8c200000 r--s 038bb000 08:05 1447960 /usr/lib/jvm/java-6-openjdk/jre/lib/rt.jar -8c200000-8c2fd000 rw-p 00000000 00:00 0 -8c2fd000-8c300000 ---p 00000000 00:00 0 -8c302000-8c306000 r--s 0007c000 08:05 1462994 /usr/lib/jvm/java-6-openjdk/jre/lib/jsse.jar -8c306000-8c30f000 r--s 00065000 08:05 919509 /usr/share/java/gnome-java-bridge.jar -8c30f000-8c310000 ---p 00000000 00:00 0 -8c310000-8c3c2000 rw-p 00000000 00:00 0 -8c3c2000-8c3c3000 ---p 00000000 00:00 0 -8c3c3000-8c443000 rw-p 00000000 00:00 0 -8c443000-8c444000 ---p 00000000 00:00 0 -8c444000-8c4d6000 rw-p 00000000 00:00 0 -8c4d6000-8c504000 rw-p 00000000 00:00 0 -8c504000-8c516000 rw-p 00000000 00:00 0 -8c516000-8c5af000 rw-p 00000000 00:00 0 -8c5af000-8c5c1000 rw-p 00000000 00:00 0 -8c5c1000-8c5ef000 rw-p 00000000 00:00 0 -8c5ef000-8c601000 rw-p 00000000 00:00 0 -8c601000-8c699000 rw-p 00000000 00:00 0 -8c699000-8c6c8000 rw-p 00000000 00:00 0 -8c6c8000-8c6ef000 rw-p 00000000 00:00 0 -8c6ef000-8e970000 rw-p 00000000 00:00 0 -8e970000-946f0000 rw-p 00000000 00:00 0 -946f0000-96a70000 rw-p 00000000 00:00 0 -96a70000-a9c50000 rw-p 00000000 00:00 0 -a9c50000-af7a0000 rw-p 00000000 00:00 0 -af7a0000-b46f0000 rw-p 00000000 00:00 0 -b46f2000-b46fd000 rw-p 00000000 00:00 0 -b46fd000-b47b2000 rw-p 00000000 00:00 0 -b47b2000-b4a52000 rwxp 00000000 00:00 0 -b4a52000-b77b2000 rw-p 00000000 00:00 0 -b77b2000-b77b5000 ---p 00000000 00:00 0 -b77b5000-b7806000 rw-p 00000000 00:00 0 -b7808000-b780b000 r--s 0000f000 08:05 1462983 /usr/lib/jvm/java-6-openjdk/jre/lib/ext/pulse-java.jar -b780b000-b780d000 r--s 0001d000 08:05 1462999 /usr/lib/jvm/java-6-openjdk/jre/lib/plugin.jar -b780d000-b7812000 r--s 00044000 08:05 1462998 /usr/lib/jvm/java-6-openjdk/jre/lib/netx.jar -b7812000-b781a000 rw-s 00000000 08:05 1448211 /tmp/hsperfdata_gadei/5529 -b781a000-b781b000 rw-p 00000000 00:00 0 -b781b000-b781c000 r--p 00000000 00:00 0 -b781c000-b781e000 rw-p 00000000 00:00 0 -bfb5c000-bfb71000 rw-p 00000000 00:00 0 [stack] - -VM Arguments: -java_command: scala.tools.nsc.Main @/tmp/scalac-ant-8019952260520385401.args -Launcher Type: SUN_STANDARD - -Environment Variables: -PATH=/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin:/usr/games -USERNAME=gadei -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 -SHELL=/bin/bash -DISPLAY=:0.0 - -Signal Handlers: -SIGSEGV: [libjvm.so+0x637540], sa_mask[0]=0x7ffbfeff, sa_flags=0x10000004 -SIGBUS: [libjvm.so+0x637540], sa_mask[0]=0x7ffbfeff, sa_flags=0x10000004 -SIGFPE: [libjvm.so+0x50e650], sa_mask[0]=0x7ffbfeff, sa_flags=0x10000004 -SIGPIPE: [libjvm.so+0x50e650], sa_mask[0]=0x7ffbfeff, sa_flags=0x10000004 -SIGXFSZ: [libjvm.so+0x50e650], sa_mask[0]=0x7ffbfeff, sa_flags=0x10000004 -SIGILL: [libjvm.so+0x50e650], sa_mask[0]=0x7ffbfeff, sa_flags=0x10000004 -SIGUSR1: SIG_DFL, sa_mask[0]=0x00000000, sa_flags=0x00000000 -SIGUSR2: [libjvm.so+0x50dd00], sa_mask[0]=0x00000004, sa_flags=0x10000004 -SIGHUP: [libjvm.so+0x510870], sa_mask[0]=0x7ffbfeff, sa_flags=0x10000004 -SIGINT: SIG_IGN, sa_mask[0]=0x00000000, sa_flags=0x00000000 -SIGTERM: [libjvm.so+0x510870], sa_mask[0]=0x7ffbfeff, sa_flags=0x10000004 -SIGQUIT: [libjvm.so+0x510870], sa_mask[0]=0x7ffbfeff, sa_flags=0x10000004 - - ---------------- S Y S T E M --------------- - -OS:Ubuntu 10.04 (lucid) -uname:Linux 2.6.32-28-generic #55-Ubuntu SMP Mon Jan 10 21:21:01 UTC 2011 i686 -libc:glibc 2.11.1 NPTL 2.11.1 -rlimit: STACK 8192k, CORE 0k, NPROC infinity, NOFILE 1024, AS infinity -load average:1.12 0.69 0.64 - -/proc/meminfo: -MemTotal: 2027000 kB -MemFree: 71488 kB -Buffers: 114588 kB -Cached: 1036544 kB -SwapCached: 0 kB -Active: 1184100 kB -Inactive: 629644 kB -Active(anon): 610028 kB -Inactive(anon): 112804 kB -Active(file): 574072 kB -Inactive(file): 516840 kB -Unevictable: 0 kB -Mlocked: 0 kB -HighTotal: 1152712 kB -HighFree: 1736 kB -LowTotal: 874288 kB -LowFree: 69752 kB -SwapTotal: 4288504 kB -SwapFree: 4288504 kB -Dirty: 92 kB -Writeback: 0 kB -AnonPages: 662552 kB -Mapped: 122776 kB -Shmem: 60220 kB -Slab: 82612 kB -SReclaimable: 67088 kB -SUnreclaim: 15524 kB -KernelStack: 2632 kB -PageTables: 6552 kB -NFS_Unstable: 0 kB -Bounce: 0 kB -WritebackTmp: 0 kB -CommitLimit: 5302004 kB -Committed_AS: 1524016 kB -VmallocTotal: 122880 kB -VmallocUsed: 38656 kB -VmallocChunk: 58164 kB -HardwareCorrupted: 0 kB -HugePages_Total: 0 -HugePages_Free: 0 -HugePages_Rsvd: 0 -HugePages_Surp: 0 -Hugepagesize: 4096 kB -DirectMap4k: 16376 kB -DirectMap4M: 892928 kB - - -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 - -Memory: 4k page, physical 2027000k(71488k free), swap 4288504k(4288504k free) - -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 - -time: Fri Jan 28 16:56:05 2011 -elapsed time: 10 seconds - diff -r f6a001b47a84 -r 6548da70f14e test/Tools/isac/Frontend/interface.sml --- a/test/Tools/isac/Frontend/interface.sml Sat Jun 18 11:28:10 2011 +0200 +++ b/test/Tools/isac/Frontend/interface.sml Mon Jun 20 17:33:06 2011 +0200 @@ -140,6 +140,7 @@ val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1; setNextTactic 1 (Apply_Method ["Test","solve_linear"]); + (*ERROR.110620 .. end-of-calculation*) val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1; is_complete_mod ptp; is_complete_spec ptp; @@ -167,8 +168,9 @@ (*exception just above means: 'ModSpec' has been returned: error anyway*) if term2str f = "[x = 1]" then () else error "FE-Kernel-interface.sml: diff.behav. in solve_linear as rootpbl"; +============ inhibit exn 110310 ==============================================*) - +(*========== inhibit exn 110620 ================================================ "--------- inspect the CalcTree No.1 with Iterator No.2 -"; "--------- inspect the CalcTree No.1 with Iterator No.2 -"; "--------- inspect the CalcTree No.1 with Iterator No.2 -"; @@ -191,7 +193,7 @@ if get_pos 1 1 = ([], Res) then () else error "FE-interface.sml: diff.behav. in b inspect 1 with Iterator 2"; moveActiveCalcHead 1; refFormula 1 ([],Pbl); - +============ inhibit exn 110620 ==============================================*) "--------- miniscript with mini-subpbl ------------------"; "--------- miniscript with mini-subpbl ------------------"; @@ -316,7 +318,6 @@ DEconstrCalcTree 1; - "--------- mini-subpbl AUTOCALCULATE Step 1 -------------"; "--------- mini-subpbl AUTOCALCULATE Step 1 -------------"; "--------- mini-subpbl AUTOCALCULATE Step 1 -------------"; @@ -369,6 +370,7 @@ DEconstrCalcTree 1; +(*========== inhibit exn 110620 ================================================ "--------- solve_linear as rootpbl AUTO CompleteCalc ----"; "--------- solve_linear as rootpbl AUTO CompleteCalc ----"; "--------- solve_linear as rootpbl AUTO CompleteCalc ----"; @@ -392,7 +394,6 @@ if term2str f = "[x = 1]" andalso p = ([], Res) then () else error "FE-interface.sml: diff.behav. in solve_linear/rt AUTOCALCULATE "; - "--------- solve_linear as rootpbl AUTO CompleteHead/Calc "; "--------- solve_linear as rootpbl AUTO CompleteHead/Calc "; "--------- solve_linear as rootpbl AUTO CompleteHead/Calc "; @@ -408,13 +409,11 @@ refFormula 1 (get_pos 1 1); val ((pt,p),_) = get_calc 1; - - autoCalculate 1 CompleteCalc; val ((pt,p),_) = get_calc 1; if p=([], Res) then () else error "FE-interface.sml: diff.behav. in solve_linear AUTOC Head/Calc "; - +============ inhibit exn 110620 ==============================================*) "--------- mini-subpbl AUTOCALCULATE CompleteCalc -------"; "--------- mini-subpbl AUTOCALCULATE CompleteCalc -------"; @@ -441,11 +440,15 @@ val ((pt,_),_) = get_calc 1; val p = get_pos 1 1; +(*========== inhibit exn 110620 ================================================ val (Form f, tac, asms) = pt_extract (pt, p); +(* ModSpec........... = ...................DIFFERENT !*) if term2str f = "[x = 1]" andalso p = ([], Res) then () else error "FE-interface.sml: diff.behav. in mini-subpbl AUTOCALCULATE 6"; +============ inhibit exn 110620 ==============================================*) +(*=== inhibit exn ?============================================================= "--------- mini-subpbl AUTO CompleteCalcHead ------------"; "--------- mini-subpbl AUTO CompleteCalcHead ------------"; "--------- mini-subpbl AUTO CompleteCalcHead ------------"; @@ -454,6 +457,7 @@ ("Test", ["sqroot-test","univariate","equation","test"], ["Test","squ-equ-test-subpbl1"]))]; Iterator 1; + moveActiveRoot 1; (* doesn't terminate !!! autoCalculate 1 CompleteCalcHead; *) @@ -1314,4 +1318,5 @@ if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else error "FE-interface.sml: diff.behav. in FORMULA:replace} NOTok"; -============ inhibit exn 110310 ==============================================*) +===== inhibit exn ?===========================================================*) + diff -r f6a001b47a84 -r 6548da70f14e test/Tools/isac/Test_Isac.thy --- a/test/Tools/isac/Test_Isac.thy Sat Jun 18 11:28:10 2011 +0200 +++ b/test/Tools/isac/Test_Isac.thy Mon Jun 20 17:33:06 2011 +0200 @@ -12,7 +12,15 @@ Isac "Knowledge/Rational_Test" "ADDTESTS/Ctxt" + "ADDTESTS/test-depend/Build_Test" "ADDTESTS/All_Ctxt" +(*"ADDTESTS/course/T2_Rewriting" theory has not been declared*) +(*"ADDTESTS/course/T1_Basics.thy" could not find ^^^*) +(*"ADDTESTS/course/T3_MathEngine" could not find ^^^*) + "ADDTESTS/file-depend/Build_Test" + "../../Pure/Isar/Test_Parsers" +(*"../../Pure/Isar/Pure/Isar/Struct_Deriv" update 2009-2-->2011*) + "../../Pure/Isar/Test_Parse_Term" uses ( "library.sml") @@ -131,7 +139,23 @@ ML {*"%%%%%%%%%%%%%%%%% start Frontend.thy %%%%%%%%%%%%%%%%%%%";*} use "Frontend/messages.sml" (*new 2011*) use "Frontend/states.sml" (*new 2011*) - use "Frontend/interface.sml" (*part.*) + use "Frontend/interface.sml" (*part.*) +ML {* + +*} +ML {* + +*} +ML {* + +*} +ML {* + +*} +ML {* + +*} + use "print_exn_G.sml" (*new 2011*) ML {*"%%%%%%%%%%%%%%%%% end Frontend.thy %%%%%%%%%%%%%%%%%%%%%";*} ML {*"%%%%%%%%%%%%%%%%% start Knowledge.thy %%%%%%%%%%%%%%%%%%";*} @@ -171,11 +195,16 @@ ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*} ML {* -*} -ML {* -*} - ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*} -ML {* +"--------- mini-subpbl AUTO CompleteCalcHead ------------"; + states:=[]; + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], + ("Test", ["sqroot-test","univariate","equation","test"], + ["Test","squ-equ-test-subpbl1"]))]; + Iterator 1; + moveActiveRoot 1; +(* doesn't terminate !!!*) + autoCalculate 1 CompleteCalcHead; +val (ModSpec (x1,x2,x3,x4,x5,x6), tac, asms) = pt_extract (pt, p); *} ML {* *} @@ -183,20 +212,19 @@ *} ML {* *} -ML {* -*} + ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*} end (*=== inhibit exn ?============================================================= ===== inhibit exn ?===========================================================*) -(*========== inhibit exn 110520 ================================================ +(*========== inhibit exn 110620 ================================================ "########### testcode inserted vvv ###########################################"; "########### testcode inserted ^^^ ###########################################"; -============ inhibit exn 110520 ==============================================*) +============ inhibit exn 110620 ==============================================*) (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-. -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)