1.1 --- a/src/Pure/Isar/toplevel.ML	Sat Feb 27 16:59:41 2021 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Mon Mar 01 12:46:40 2021 +0100
     1.3 @@ -361,6 +361,7 @@
     1.4  
     1.5  fun at_command tr = command_msg "At " tr;
     1.6  fun type_error tr = command_msg "Bad context for " tr;
     1.7 +fun type_error tr = (writeln "#### type_error"; command_msg "Bad context for " tr);
     1.8  
     1.9  
    1.10  (* modify transitions *)

     2.1 --- a/src/Pure/PIDE/command.ML	Sat Feb 27 16:59:41 2021 +0100
     2.2 +++ b/src/Pure/PIDE/command.ML	Mon Mar 01 12:46:40 2021 +0100
     2.3 @@ -197,13 +197,14 @@
     2.4    let
     2.5      val name = Toplevel.name_of tr;
     2.6      val res =
     2.7 -      if Keyword.is_theory_body keywords name then Toplevel.reset_theory st0
     2.8 -      else if Keyword.is_proof keywords name then Toplevel.reset_proof st0
     2.9 +      if Keyword.is_theory_body keywords name then (writeln "#### is_theory_body"; Toplevel.reset_theory st0)
    2.10 +      else if Keyword.is_proof keywords name then (writeln "#### is_proof"; Toplevel.reset_proof st0)
    2.11        else if Keyword.is_theory_end keywords name then
    2.12          (case Toplevel.reset_notepad st0 of
    2.13            NONE => Toplevel.reset_theory st0
    2.14          | some => some)
    2.15        else NONE;
    2.16 +    val _ = @{print}{a = "#### reset_state", name = name, res = res, st0 = st0, tr = tr}
    2.17    in
    2.18      (case res of
    2.19        NONE => st0

     3.1 --- a/src/Tools/isac/BridgeJEdit/Calculation.thy	Sat Feb 27 16:59:41 2021 +0100
     3.2 +++ b/src/Tools/isac/BridgeJEdit/Calculation.thy	Mon Mar 01 12:46:40 2021 +0100
     3.3 @@ -14,7 +14,7 @@
     3.4      "Example" :: thy_load ("str") (* "spark_vc" :: thy_goal *)
     3.5    and "Problem" :: thy_decl (* root-problem + recursively in Solution;
     3.6                                 "spark_vc" :: thy_goal *)
     3.7 -  and "Specification" "Model" :: prf_chain
     3.8 +  and "Specification" "Model" :: diag
     3.9    and "References" "Solution" :: prf_chain (* structure only *)
    3.10    and "Where" "Given" "Find" "Relate" :: prf_chain (* await input of term, cp.from "from".."have" *)
    3.11  (*and "Where" (* only output, preliminarily *)*)
    3.12 @@ -145,7 +145,20 @@
    3.13        ParseC.problem_headline -> Toplevel.transition -> Toplevel.transition;(**)
    3.14  (*                               ^^^^^^^^^^^^^^^^^^^    ^^^^^^^^^^^^^^^^^^^*)
    3.15  \<close> ML \<open>
    3.16 -fun dummy (_: string) thy = thy;
    3.17 +\<close> ML \<open>
    3.18 +OMod_Data.get
    3.19 +\<close> ML \<open>
    3.20 +fun dummy (_(*":"*): string) thy =
    3.21 +  let
    3.22 +    val refs' = Refs_Data.get thy
    3.23 +    val o_model = OMod_Data.get thy
    3.24 +    val i_model = IMod_Data.get thy
    3.25 +    val _ =
    3.26 +      @{print} {a = "### dummy Specification", refs = refs', o_model = o_model, i_model = i_model}
    3.27 +  in
    3.28 +    thy
    3.29 +  end;
    3.30 +\<close> ML \<open>
    3.31  (Toplevel.theory o dummy): string -> Toplevel.transition -> Toplevel.transition
    3.32  \<close> ML \<open>
    3.33  val _ =
    3.34 @@ -153,13 +166,11 @@
    3.35      (Parse.input Parse.cartouche >> (fn input =>
    3.36        Toplevel.keep (fn _ => ignore (ML_Lex.read_source (*true*) input))))
    3.37  *)Outer_Syntax.command \<^command_keyword>\<open>Specification\<close> "Specification dummy"
    3.38 -    ((writeln o Token.s_to_string, Parse.$$$ ":") 
    3.39 -      @@>> (Toplevel.theory o dummy))
    3.40 +    ((writeln o Token.s_to_string, Parse.$$$ ":") @@>> (Toplevel.theory o dummy))
    3.41  \<close> ML \<open>
    3.42  val _ =
    3.43    Outer_Syntax.command \<^command_keyword>\<open>Model\<close> "Model dummy"
    3.44 -    ((writeln o Token.s_to_string, Parse.$$$ ":") 
    3.45 -      @@>> (fn _ => Toplevel.keep (fn _ => ignore (writeln ""))))
    3.46 +    ((writeln o Token.s_to_string, Parse.$$$ ":") @@>> (Toplevel.theory o dummy))
    3.47  \<close> ML \<open>
    3.48  val _ =
    3.49    Outer_Syntax.command \<^command_keyword>\<open>Given\<close> "input Given items to the Model of a Specification"
    3.50 @@ -214,10 +225,10 @@
    3.51  
    3.52  Problem ("Biegelinie", ["Biegelinien"])
    3.53  (*1 collapse* )
    3.54 -  Specification:                 (*Bad context for command "Specification"\<^here> -- using reset state*)
    3.55 +  Specification:
    3.56    (*2 collapse*)
    3.57      Model:
    3.58 -      Given: "Traegerlaenge " "Streckenlast "              
    3.59 +      Given: "Traegerlaenge " "Streckenlast " (*Bad context for command "Given"\<^here> -- using reset state*)
    3.60        Where: "q_0 ist_integrierbar_auf {| 0, L |}" "0 < L"
    3.61        Find: "Biegelinie "
    3.62        Relate: "Randbedingungen "
    3.63 @@ -229,7 +240,7 @@
    3.64        (*3 collapse*)
    3.65    (*2 collapse*)
    3.66    Solution:
    3.67 -( *1 collapse*)
    3.68 +( * 1 collapse*)
    3.69  (*
    3.70    compare click on above Given: "Traegerlaenge ", "Streckenlast " 
    3.71    with click on from \<open>0 < d\<close> in SPARK/../Greatest_Common_Divisorthy