1.1 --- a/src/Tools/isac/BridgeJEdit/preliminary.sml	Wed Feb 03 16:39:44 2021 +0100
     1.2 +++ b/src/Tools/isac/BridgeJEdit/preliminary.sml	Thu Feb 11 17:45:29 2021 +0100
     1.3 @@ -10,8 +10,8 @@
     1.4  sig
     1.5    (* for keyword Example *)
     1.6    val store_and_show: theory -> Formalise.T list -> theory -> theory;
     1.7 -  val load_formalisation: theory ->(Fdl_Lexer.T list -> ParseC.form_model_refs * 'a) ->
     1.8 -  (theory -> Token.file list * theory) * 'c -> theory -> theory
     1.9 +  val load_formalisation: theory -> (Fdl_Lexer.T list -> ParseC.form_model_refs * 'a) ->
    1.10 +    (theory -> Token.file list * theory) * 'c -> theory -> theory
    1.11    
    1.12    (* for keyword Problem*)
    1.13  (**)val prove_vc: ParseC.problem -> Proof.context -> Proof.state(**)
    1.14 @@ -37,6 +37,13 @@
    1.15    val extend = I
    1.16    fun merge (_, o_model) = o_model
    1.17  );
    1.18 +structure IMod_Data = Theory_Data
    1.19 +(
    1.20 +  type T = I_Model.T
    1.21 +  val empty : T = []
    1.22 +  val extend = I
    1.23 +  fun merge (_, i_model) = i_model
    1.24 +);
    1.25  structure Ctxt_Data = Theory_Data
    1.26  (
    1.27    type T = Proof.context
    1.28 @@ -91,7 +98,7 @@
    1.29        |> fst
    1.30        |> ParseC.read_out_formalise
    1.31        |> store_and_show HACKthy
    1.32 -(** )val _ = @{print} {a = "### load_formalisation \<rightarrow>", formalise = formalise}( **)
    1.33 +(**)val _ = @{print} {a = "### load_formalisation \<rightarrow>", formalise = formalise}(**)
    1.34    in
    1.35      formalise thy'
    1.36    end;
    1.37 @@ -586,6 +593,7 @@
    1.38  
    1.39  (** copied from spark_commands.ML **)
    1.40  
    1.41 +(*  get_vc: theory -> string -> (typ, term, thm list) Element.ctxt list * ('a, term) Element.stmt *)
    1.42  fun get_vc thy vc_name =
    1.43    (case SPARK_VCs.lookup_vc thy false vc_name of
    1.44      SOME (ctxt, (_, proved, ctxt', stmt)) =>
    1.45 @@ -603,24 +611,26 @@
    1.46    then ((thy, pbl, met_id) : References.T, o_model)
    1.47    else ((inthy, inpbl, MethodC.id_empty), [])
    1.48  
    1.49 -fun prove_vc (*vc_name*)problem lthy =
    1.50 +fun prove_vc (*vc_name*)problem lthy(*Proof.context*) =
    1.51    let
    1.52      val _ = @{print} {a = "//--- Spark_Commands.prove_vc", headline = problem}
    1.53      val thy = Proof_Context.theory_of lthy;
    1.54      val vc_name = "procedure_g_c_d_4" (*fixed for spark_open \<open>greatest_common_divisor/g_c_d\<close>*)
    1.55 -    val (ctxt, stmt) = get_vc thy vc_name
    1.56 +    val (ctxt(*Element.context_i list*), stmt) = get_vc thy vc_name
    1.57  (*//--------------------------------- new code --------------------------------\\*)
    1.58  (**)val {thy_id, pbl_id, (*givens, wheres, ..*)...} = ParseC.read_out_problem problem(*_headline*)
    1.59  (** )val (thy_id, pbl_id) = ParseC.read_out_headline problem( *_headline*)
    1.60      val refs' = Refs_Data.get thy
    1.61      val (refs as (_, pbl_id, _), o_model) = prefer_input (thy_id, pbl_id) refs' (OMod_Data.get thy)
    1.62      val i_model = I_Model.initPIDE pbl_id
    1.63 +    val thy = IMod_Data.put i_model (* the Model-items with Descriptor only *)
    1.64  (*
    1.65    TODO: present Specification = i_model () + refs via PIDE
    1.66  *)
    1.67  (*----------------------------------- new code ----------------------------------*)
    1.68      val _ = @{print} {a = "prove_vc", o_model = o_model, refs = refs, i_model = i_model}
    1.69  (*\\--------------------------------- new code --------------------------------//*)
    1.70 +    val ctxt = ctxt
    1.71    in
    1.72      Specification.theorem true Thm.theoremK NONE
    1.73        (fn thmss => (Local_Theory.background_theory