1.1 --- a/src/Tools/isac/BridgeJEdit/Calculation.thy	Wed Feb 03 14:53:37 2021 +0100
     1.2 +++ b/src/Tools/isac/BridgeJEdit/Calculation.thy	Wed Feb 03 15:21:12 2021 +0100
     1.3 @@ -59,7 +59,7 @@
     1.4  \<close> ML \<open>
     1.5  \<close>
     1.6  
     1.7 -section \<open>setup command_keyword \<close>
     1.8 +section \<open>setup command_keyword + preliminary test\<close>
     1.9  ML \<open>
    1.10  \<close> ML \<open>
    1.11  val _ =                                                  
    1.12 @@ -71,9 +71,11 @@
    1.13  val _ =
    1.14    Outer_Syntax.local_theory_to_proof \<^command_keyword>\<open>Problem\<close>
    1.15      "start a Specification, either from scratch or from preceding 'Example'"
    1.16 -    (ParseC.problem >> Preliminary.prove_vc);
    1.17 +(**)(ParseC.problem >> Preliminary.prove_vc);(**)
    1.18 +(** )(ParseC.problem_headline >> Preliminary.prove_vc);( **)
    1.19  \<close> ML \<open>
    1.20 -Preliminary.prove_vc: ParseC.problem -> Proof.context -> Proof.state;
    1.21 +(**)Preliminary.prove_vc: ParseC.problem -> Proof.context -> Proof.state;(**)
    1.22 +(** )Preliminary.prove_vc: ParseC.problem_headline -> Proof.context -> Proof.state;( **)
    1.23  SPARK_Commands.prove_vc: string -> Proof.context -> Proof.state
    1.24  \<close> ML \<open>
    1.25  \<close> ML \<open> (*-----------------------------------------------------------------------------------*)
    1.26 @@ -91,7 +93,7 @@
    1.27  \<close> ML \<open>
    1.28  \<close>
    1.29  
    1.30 -subsection \<open>test runs with Example\<close>
    1.31 +subsection \<open>test runs with test-Example\<close>
    1.32  (**)
    1.33  Example \<open>/usr/local/isabisac/src/Tools/isac/Examples/exp_Statics_Biegel_Timischl_7-70\<close>
    1.34  (*(1) outcomment before creating session Isac* )
    1.35 @@ -99,16 +101,16 @@
    1.36  (*makes Outer_Syntax..Problem run; Isac code is just added..*)
    1.37  spark_open \<open>~~/src/HOL/SPARK/Examples/Gcd/greatest_common_divisor/g_c_d\<close>
    1.38  
    1.39 -( *(2) outcomment before creating session Isac* )
    1.40 +(*(2) outcomment before creating session Isac*)
    1.41  Problem ("Biegelinie", ["Biegelinien"]) (*procedure_g_c_d_4 .."Problem" adds to SPARK*)
    1.42 -  Specification:
    1.43 +  Specification:                                               (*Outer syntax error\<^here>: command expected, but keyword Specification\<^here> was found*)
    1.44  (*1 collapse*)
    1.45      Model:
    1.46        Given: "Traegerlaenge "(*,*) "Streckenlast "
    1.47 -      Where: "q_0 ist_integrierbar_auf {| 0, L |}"(*,*) "0 < L"
    1.48 -      Find: "Biegelinie "
    1.49 +      Where: "q_0 ist_integrierbar_auf {| 0, L |}"(*,*) "0 < L"(*Outer syntax error\<^here>: command expected, but keyword Where\<^here> was found*)
    1.50 +      Find: "Biegelinie "                                      (*Bad context for command "Find"\<^here> -- using reset state*)
    1.51        Relate: "Randbedingungen "
    1.52 -    References:
    1.53 +    References:                                                 (*Outer syntax error\<^here>: command expected, but keyword References\<^here> was found*)
    1.54    (*2 collapse*)
    1.55        RTheory: ""
    1.56        RProblem: ["", ""]
    1.57 @@ -116,7 +118,7 @@
    1.58    (*2 collapse*)
    1.59  (*1 collapse*)
    1.60    Solution:
    1.61 -( **)
    1.62 +( *(1) outcomment before creating session Isac*)
    1.63  (*
    1.64    compare click on above Given: "Traegerlaenge ", "Streckenlast " 
    1.65    with click on from \<open>0 < d\<close> in SPARK/../Greatest_Common_Divisorthy

     2.1 --- a/src/Tools/isac/BridgeJEdit/preliminary.sml	Wed Feb 03 14:53:37 2021 +0100
     2.2 +++ b/src/Tools/isac/BridgeJEdit/preliminary.sml	Wed Feb 03 15:21:12 2021 +0100
     2.3 @@ -14,7 +14,8 @@
     2.4    (theory -> Token.file list * theory) * 'c -> theory -> theory
     2.5    
     2.6    (* for keyword Problem*)
     2.7 -  val prove_vc: ParseC.problem -> Proof.context -> Proof.state
     2.8 +(**)val prove_vc: ParseC.problem -> Proof.context -> Proof.state(**)
     2.9 +(** )val prove_vc: ParseC.problem_headline -> Proof.context -> Proof.state( **)
    2.10  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    2.11  (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    2.12  ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    2.13 @@ -601,9 +602,7 @@
    2.14    if inthy = thy andalso inpbl = pbl
    2.15    then ((thy, pbl, met_id) : References.T, o_model)
    2.16    else ((inthy, inpbl, Method.id_empty), [])
    2.17 -(*
    2.18 -val prove_vc: ParseC.problem((_headline)) -> Proof.context -> Proof.state
    2.19 -*)
    2.20 +
    2.21  fun prove_vc (*vc_name*)problem lthy =
    2.22    let
    2.23      val _ = @{print} {a = "//--- Spark_Commands.prove_vc", headline = problem}