(*  Title:      Tools/isac/BridgeJEdit/preliminary-OLD..sml

     Author:     Walther Neuper, JKU Linz

     (c) due to copyright terms

 Preliminary code for start transition Libisabelle -- PIDE.

 Will be distributed to several structures, most of which do not yet exist.

 *)

 signature PRELIMINARY_OLD =

 sig

   (* for keyword ExampleSPARK *)

   val store_and_show: theory -> Formalise.T list -> theory -> theory;

   val load_formalisation: theory -> (Fdl_Lexer.T list -> ParseC_OLD.form_model_refs * 'a) ->

     (theory -> Token.file * theory) * string -> theory -> theory

   (* for keyword Problem*)

 (**)val init_specify: ParseC_OLD.problem_headline -> theory -> theory(**)

 (** )val init_specify: ParseC_OLD.problem -> theory -> theory( **)

 end

 (** code for keyword ExampleSPARK **)

 structure Refs_Data = Theory_Data

 (

   type T = References.T

   val empty : T = References.empty

   val extend = I

   fun merge (_, refs) = refs

 );

 structure OMod_Data = Theory_Data

 (

   type T = O_Model.T

   val empty : T = []

   val extend = I

   fun merge (_, o_model) = o_model

 );

 structure IMod_Data = Theory_Data

 (

   type T = I_Model.T

   val empty : T = []

   val extend = I

   fun merge (_, i_model) = i_model

 );

 structure Ctxt_Data = Theory_Data

 (

   type T = Proof.context

   val empty : T = ContextC.empty

   val extend = I

   fun merge (_, ctxt) = ctxt

 );

 (**)

 structure Preliminary_OLD(**): PRELIMINARY_OLD(**) =

 struct

 (**)

 fun store_and_show HACKthy formalise thy =

   let

 (**)val _(*file_read_correct*) = case formalise of xxx as

       [(["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y", "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]", "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]", "AbleitungBiegelinie dy"],

         ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]))] => hd xxx

       | _ => error "magic failed: handling file exp_Statics_Biegel_Timischl_7-70.str failed"

 (**)

     val formalise = hd formalise (*we expect only one Formalise.T in the list*)

     val (_(*hdlPIDE*), _, refs, o_model, var_type_ctxt) = Step_Specify.initialisePIDEHACK HACKthy formalise

   (*              ^^ TODO remove with cleanup in nxt_specify_init_calc *)

 (*

   TODO: present "Problem hdlPIDE" via PIDE

 *)

   in

     thy

       |> Refs_Data.put refs

       |> OMod_Data.put o_model

       |> Ctxt_Data.put var_type_ctxt

   end;

 (*

 fun load_formalisation parser (files, _) thy =

   let

     val ([{lines, pos, ...}: Token.file], thy') = files thy;

   in

     store_and_show

       (ParseC_OLD.read_out_formalise (fst (parser (fst (ParseC_OLD.tokenize_formalise pos (cat_lines lines))))))

         thy'

   end;

 *)

 fun load_formalisation HACKthy parse (get_file: theory -> Token.file * theory, _: string) thy =

   let

     val (file, thy') = get_file thy;

     val formalise = #lines file

       |> cat_lines 

       |> ParseC_OLD.tokenize_formalise (#pos file)

       |> fst

       |> parse

       |> fst

       |> ParseC_OLD.read_out_formalise

       |> store_and_show HACKthy

 (**)val _ = @{print} {a = "### load_formalisation \<rightarrow>", formalise = formalise}(**)

   in

     formalise thy'

   end;

 (*** code for keyword Problem ***)

 (*

 val prefer_input: ThyC.id * Problem.id -> References.T -> O_Model.T -> References.T * O_Model.T

 *)

 fun prefer_input (inthy, inpbl : Problem.id) (thy, pbl, met_id) o_model =

   if inthy = thy andalso inpbl = pbl

   then ((thy, pbl, met_id) : References.T, o_model)

   else ((inthy, inpbl, MethodC.id_empty), [])

 fun init_specify problem thy =

   let

     val _ = @{print} {a = "//--- Spark_Commands.init_specify", headline = problem}

     val (thy_id, pbl_id) = ParseC_OLD.read_out_headline problem (*how handle Position?!?*)

     val refs' = Refs_Data.get thy

     val ((_, pbl_id, _), _(*o_model*)) =

       prefer_input (thy_id, pbl_id) refs' (OMod_Data.get thy)

     val i_model = I_Model.initPIDE pbl_id

 (* TODO: present Specification = i_model + refs via PIDE, if specify is done explicitly. *)

   in

     IMod_Data.put i_model thy (* the Model-items with Descriptor s only *)

   end;

 (**)

 (**)end(**)