(*  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

  (* for keyword Example *)

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

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

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

  (* for keyword Problem*)

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

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

end

(** code for keyword Example **)

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(**): PRELIMINARY(**) =

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.read_out_formalise (fst (parser (fst (ParseC.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.tokenize_formalise (#pos file)

      |> fst

      |> parse

      |> fst

      |> ParseC.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.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(**)