Test_Some Example reports no error and no <Output>
authorWalther Neuper <walther.neuper@jku.at>
Sat, 28 Nov 2020 17:47:43 +0100
changeset 601188b008da6c2ef
parent 60117 3ea616c84845
child 60119 2792efa4a5de
Test_Some Example reports no error and no <Output>
src/Tools/isac/BridgeJEdit/Calculation.thy
test/Tools/isac/Test_Some.thy
     1.1 --- a/src/Tools/isac/BridgeJEdit/Calculation.thy	Fri Nov 27 20:54:01 2020 +0100
     1.2 +++ b/src/Tools/isac/BridgeJEdit/Calculation.thy	Sat Nov 28 17:47:43 2020 +0100
     1.3 @@ -118,11 +118,12 @@
     1.4  
     1.5  subsection \<open>test runs with Example\<close>
     1.6  text \<open>
     1.7 -  Do in Test_Some.thy:
     1.8 +  Starting the Calculation for the Example requires session Isac with Isac.Biegelinie etc.
     1.9 +  So, do ~~$ ./zcoding-to-test.sh and use Test_Some.thy to evaluate
    1.10  
    1.11      Example \<open>/usr/local/isabisac/src/Tools/isac/Examples/exp_Statics_Biegel_Timischl_7-70\<close>
    1.12  
    1.13 -  Starting the Calculation for the Example requires session Isac with Isac.Biegelinie etc.
    1.14 +  This now gives no error, but also no <Output>. See child of 3ea616c84845.
    1.15  \<close>
    1.16  
    1.17  section \<open>Adapt Sledgehammer to write Problem ("Biegelinie", ["Biegelinien"]) to thy\<close>
     2.1 --- a/test/Tools/isac/Test_Some.thy	Fri Nov 27 20:54:01 2020 +0100
     2.2 +++ b/test/Tools/isac/Test_Some.thy	Sat Nov 28 17:47:43 2020 +0100
     2.3 @@ -95,14 +95,11 @@
     2.4  
     2.5  section \<open>===================================================================================\<close>
     2.6  ML \<open>
     2.7 -\<close> ML \<open>
     2.8  @{theory Calculation}
     2.9  \<close> ML \<open>
    2.10  @{theory Biegelinie}
    2.11  \<close> ML \<open>
    2.12 -\<close> ML \<open>
    2.13  \<close>
    2.14 -
    2.15  Example \<open>/usr/local/isabisac/src/Tools/isac/Examples/exp_Statics_Biegel_Timischl_7-70\<close>(*.str*)
    2.16  
    2.17