(*  Title:      Tools/isac/BridgeJEdit/preliminary.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 =

 sig

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

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

   (theory -> Token.file list * theory) * 'c -> theory -> theory

 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)

 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )

 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)

 end

 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 Ctxt_Data = Theory_Data

 (

   type T = Proof.context

   val empty : T = ContextC.empty

   val extend = I

   fun merge (_, ctxt) = ctxt

 );

 (**)

 structure Preliminary(**): PRELIMINARY(**) =

 struct

 fun store_and_show 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.initialisePIDE 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.read_out_formalise (fst (parser (fst (ParseC.tokenize_formalise pos (cat_lines lines))))))

         thy'

   end;

 *)

 fun load_formalisation parse (files, _) thy =

   let

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

     val formalise = lines

       |> cat_lines 

       |> ParseC.tokenize_formalise pos

       |> fst

       |> parse

       |> fst

       |> ParseC.read_out_formalise

       |> store_and_show

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

   in

     formalise thy'

   end;

 end