1.1 --- a/src/Tools/isac/BridgeJEdit/Calculation.thy	Sun Jan 17 13:16:25 2021 +0100
     1.2 +++ b/src/Tools/isac/BridgeJEdit/Calculation.thy	Sun Jan 17 15:25:27 2021 +0100
     1.3 @@ -22,12 +22,15 @@
     1.4  begin
     1.5  
     1.6  (**)ML_file parseC.sml(**)
     1.7 +(**)ML_file preliminary.sml(**)
     1.8 +(**)ML_file "~~/test/Tools/isac/BridgeJEdit/preliminary.sml"(*remove with next step*)
     1.9 +
    1.10  
    1.11  section \<open>new code for Outer_Syntax Example, Problem, ...\<close>
    1.12  
    1.13 -subsection \<open>code for Example\<close>
    1.14 +subsection \<open>code for Example, also needed for keyword \<open>Problem\<close>\<close>
    1.15  ML \<open>
    1.16 -\<close> ML \<open>
    1.17 +\<close> ML \<open> (*also needed for keyword \<open>Problem\<close>*)
    1.18  structure Refs_Data = Theory_Data
    1.19  (
    1.20    type T = References.T
    1.21 @@ -35,93 +38,20 @@
    1.22    val extend = I
    1.23    fun merge (_, refs) = refs
    1.24  );
    1.25 -(*/----------------------------- shift to test/../? ----------------------------------------\*)
    1.26 -(* Pure/context.ML
    1.27 -signature THEORY_DATA =
    1.28 -sig
    1.29 -  type T
    1.30 -  val get: theory -> T
    1.31 -  val put: T -> theory -> theory
    1.32 -  val map: (T -> T) -> theory -> theory
    1.33 -end;*)
    1.34 -(*
    1.35 -Refs_Data.empty;                                    (*in Refs_Data defined workers are hidden*)
    1.36 -Refs_Data.extend;                                   (*in Refs_Data defined workers are hidden*)
    1.37 -Refs_Data.merge;                                    (*in Refs_Data defined workers are hidden*)
    1.38 -ML error\<^here>:
    1.39 -Value or constructor (empty) has not been declared in structure Refs *)
    1.40 -
    1.41 -Refs_Data.get: theory -> Refs_Data.T;                            (*from signature THEORY_DATA*)
    1.42 -Refs_Data.put: Refs_Data.T -> theory -> theory;                  (*from signature THEORY_DATA*)
    1.43 -Refs_Data.map: (Refs_Data.T -> Refs_Data.T) -> theory -> theory; (*from signature THEORY_DATA*)
    1.44 -(*\----------------------------- shift to test/../? ----------------------------------------/*)
    1.45 -\<close> ML \<open>
    1.46  structure OMod_Data = Theory_Data
    1.47  (
    1.48    type T = O_Model.T
    1.49    val empty : T = []
    1.50    val extend = I
    1.51    fun merge (_, o_model) = o_model
    1.52 -)
    1.53 -\<close> ML \<open>
    1.54 +);
    1.55  structure Ctxt_Data = Theory_Data
    1.56  (
    1.57    type T = Proof.context
    1.58    val empty : T = ContextC.empty
    1.59    val extend = I
    1.60    fun merge (_, ctxt) = ctxt
    1.61 -)
    1.62 -\<close> ML \<open>
    1.63 -(*
    1.64 -store_and_show: Formalise.T list -> theory -> theory;
    1.65 -*)
    1.66 -fun store_and_show formalise thy =
    1.67 -  let
    1.68 -(**)val file_read_correct = case formalise of xxx as
    1.69 -      [(["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"],
    1.70 -        ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]))] => hd xxx
    1.71 -      | _ => error "magic failed: handling file exp_Statics_Biegel_Timischl_7-70.str failed"
    1.72 -(**)
    1.73 -    val formalise = hd formalise (*we expect only one Formalise.T in the list*)
    1.74 -    val (hdlPIDE, _, refs, o_model, var_type_ctxt) = Step_Specify.initialisePIDE formalise
    1.75 -  (*              ^^ TODO remove with cleanup in nxt_specify_init_calc *)
    1.76 -(*
    1.77 -  TODO: present "Problem hdlPIDE" via PIDE
    1.78 -*)
    1.79 -  in
    1.80 -    thy
    1.81 -      |> Refs_Data.put refs
    1.82 -      |> OMod_Data.put o_model
    1.83 -      |> Ctxt_Data.put var_type_ctxt
    1.84 -  end;
    1.85 -\<close> ML \<open>
    1.86 -store_and_show: Formalise.T list -> theory -> theory;
    1.87 -\<close> ML \<open>
    1.88 -\<close> ML \<open>
    1.89 -fun load_formalisation parser (files, _) thy =
    1.90 -  let
    1.91 -    val ([{lines, pos, ...}: Token.file], thy') = files thy;
    1.92 -  in
    1.93 -    store_and_show
    1.94 -      (ParseC.read_out_formalise (fst (parser (fst (ParseC.tokenize_formalise pos (cat_lines lines))))))
    1.95 -        thy'
    1.96 -  end;
    1.97 -fun load_formalisation parse (files, _) thy =
    1.98 -  let
    1.99 -    val ([{lines, pos, ...}: Token.file], thy') = files thy;
   1.100 -    val formalise = lines
   1.101 -      |> cat_lines 
   1.102 -      |> ParseC.tokenize_formalise pos
   1.103 -      |> fst
   1.104 -      |> parse
   1.105 -      |> fst
   1.106 -      |> ParseC.read_out_formalise
   1.107 -      |> store_and_show
   1.108 -    val _ = @{print} {a = "### load_formalisation \<rightarrow>", formalise = formalise}
   1.109 -  in
   1.110 -    formalise thy'
   1.111 -  end;
   1.112 -\<close> ML \<open>
   1.113 +);
   1.114  \<close>
   1.115  
   1.116  subsection \<open>code to write Problem ("Biegelinie", ["Biegelinien"]) to thy\<close>
   1.117 @@ -706,13 +636,17 @@
   1.118  val _ =                                                  
   1.119    Outer_Syntax.command \<^command_keyword>\<open>Example\<close> "start a Calculation from a Formalise-file"
   1.120      (Resources.provide_parse_files "Example" -- Parse.parname
   1.121 -      >> (Toplevel.theory o (load_formalisation ParseC.formalisation)));
   1.122 +      >> (Toplevel.theory o (Preliminary.load_formalisation ParseC.formalisation)));
   1.123  \<close> ML \<open>
   1.124  val _ =
   1.125    Outer_Syntax.local_theory_to_proof \<^command_keyword>\<open>Problem\<close>
   1.126      "start a Specification, either from scratch or from preceding 'Example'"
   1.127      (ParseC.problem >> prove_vc);
   1.128  \<close> ML \<open>
   1.129 +prove_vc: ParseC.problem -> Proof.context -> Proof.state
   1.130 +\<close> ML \<open>
   1.131 +SPARK_Commands.prove_vc: string -> Proof.context -> Proof.state
   1.132 +\<close> ML \<open>
   1.133  \<close>
   1.134  
   1.135  subsection \<open>test runs with Example\<close>

     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Tools/isac/BridgeJEdit/preliminary.sml	Sun Jan 17 15:25:27 2021 +0100
     2.3 @@ -0,0 +1,94 @@
     2.4 +(*  Title:      Tools/isac/BridgeJEdit/preliminary.sml
     2.5 +    Author:     Walther Neuper, JKU Linz
     2.6 +    (c) due to copyright terms
     2.7 +
     2.8 +Preliminary code for start transition Libisabelle -- PIDE.
     2.9 +Will be distributed to several structures, most of which do not yet exist.
    2.10 +*)
    2.11 +
    2.12 +signature PRELIMINARY =
    2.13 +sig
    2.14 +  val store_and_show: Formalise.T list -> theory -> theory;
    2.15 +  val load_formalisation: (Fdl_Lexer.T list -> ParseC.form_model_refs * 'a) ->
    2.16 +  (theory -> Token.file list * theory) * 'c -> theory -> theory
    2.17 +  
    2.18 +(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    2.19 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    2.20 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    2.21 +end
    2.22 +
    2.23 +structure Refs_Data = Theory_Data
    2.24 +(
    2.25 +  type T = References.T
    2.26 +  val empty : T = References.empty
    2.27 +  val extend = I
    2.28 +  fun merge (_, refs) = refs
    2.29 +);
    2.30 +structure OMod_Data = Theory_Data
    2.31 +(
    2.32 +  type T = O_Model.T
    2.33 +  val empty : T = []
    2.34 +  val extend = I
    2.35 +  fun merge (_, o_model) = o_model
    2.36 +);
    2.37 +structure Ctxt_Data = Theory_Data
    2.38 +(
    2.39 +  type T = Proof.context
    2.40 +  val empty : T = ContextC.empty
    2.41 +  val extend = I
    2.42 +  fun merge (_, ctxt) = ctxt
    2.43 +);
    2.44 +
    2.45 +(**)
    2.46 +structure Preliminary(**): PRELIMINARY(**) =
    2.47 +struct
    2.48 +
    2.49 +
    2.50 +fun store_and_show formalise thy =
    2.51 +  let
    2.52 +(**)val file_read_correct = case formalise of xxx as
    2.53 +      [(["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"],
    2.54 +        ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]))] => hd xxx
    2.55 +      | _ => error "magic failed: handling file exp_Statics_Biegel_Timischl_7-70.str failed"
    2.56 +(**)
    2.57 +    val formalise = hd formalise (*we expect only one Formalise.T in the list*)
    2.58 +    val (hdlPIDE, _, refs, o_model, var_type_ctxt) = Step_Specify.initialisePIDE formalise
    2.59 +  (*              ^^ TODO remove with cleanup in nxt_specify_init_calc *)
    2.60 +(*
    2.61 +  TODO: present "Problem hdlPIDE" via PIDE
    2.62 +*)
    2.63 +  in
    2.64 +    thy
    2.65 +      |> Refs_Data.put refs
    2.66 +      |> OMod_Data.put o_model
    2.67 +      |> Ctxt_Data.put var_type_ctxt
    2.68 +  end;
    2.69 +
    2.70 +(*
    2.71 +fun load_formalisation parser (files, _) thy =
    2.72 +  let
    2.73 +    val ([{lines, pos, ...}: Token.file], thy') = files thy;
    2.74 +  in
    2.75 +    store_and_show
    2.76 +      (ParseC.read_out_formalise (fst (parser (fst (ParseC.tokenize_formalise pos (cat_lines lines))))))
    2.77 +        thy'
    2.78 +  end;
    2.79 +*)
    2.80 +fun load_formalisation parse (files, _) thy =
    2.81 +  let
    2.82 +    val ([{lines, pos, ...}: Token.file], thy') = files thy;
    2.83 +    val formalise = lines
    2.84 +      |> cat_lines 
    2.85 +      |> ParseC.tokenize_formalise pos
    2.86 +      |> fst
    2.87 +      |> parse
    2.88 +      |> fst
    2.89 +      |> ParseC.read_out_formalise
    2.90 +      |> store_and_show
    2.91 +    val _ = @{print} {a = "### load_formalisation \<rightarrow>", formalise = formalise}
    2.92 +  in
    2.93 +    formalise thy'
    2.94 +  end;
    2.95 +
    2.96 +
    2.97 +end

     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/test/Tools/isac/BridgeJEdit/preliminary.sml	Sun Jan 17 15:25:27 2021 +0100
     3.3 @@ -0,0 +1,34 @@
     3.4 +(* Title:  "BridgeJEdit/preliminary.sml"
     3.5 +   Author: Walther Neuper
     3.6 +   (c) due to copyright terms
     3.7 +*)
     3.8 +
     3.9 +"-----------------------------------------------------------------------------------------------";
    3.10 +"table of contents -----------------------------------------------------------------------------";
    3.11 +"-----------------------------------------------------------------------------------------------";
    3.12 +"----------- investigate Pure/context.ML THEORY_DATA -------------------------------------------";
    3.13 +"-----------------------------------------------------------------------------------------------";
    3.14 +"-----------------------------------------------------------------------------------------------";
    3.15 +"-----------------------------------------------------------------------------------------------";
    3.16 +
    3.17 +"----------- investigate Pure/context.ML THEORY_DATA -------------------------------------------";
    3.18 +"----------- investigate Pure/context.ML THEORY_DATA -------------------------------------------";
    3.19 +"----------- investigate Pure/context.ML THEORY_DATA -------------------------------------------";
    3.20 +(* Pure/context.ML
    3.21 +signature THEORY_DATA =
    3.22 +sig
    3.23 +  type T
    3.24 +  val get: theory -> T
    3.25 +  val put: T -> theory -> theory
    3.26 +  val map: (T -> T) -> theory -> theory
    3.27 +end;*)
    3.28 +(*
    3.29 +Refs_Data.empty;                                    (*in Refs_Data defined workers are hidden*)
    3.30 +Refs_Data.extend;                                   (*in Refs_Data defined workers are hidden*)
    3.31 +Refs_Data.merge;                                    (*in Refs_Data defined workers are hidden*)
    3.32 +ML error:
    3.33 +Value or constructor (empty) has not been declared in structure Refs *)
    3.34 +
    3.35 +Refs_Data.get: theory -> Refs_Data.T;                            (*from signature THEORY_DATA*)
    3.36 +Refs_Data.put: Refs_Data.T -> theory -> theory;                  (*from signature THEORY_DATA*)
    3.37 +Refs_Data.map: (Refs_Data.T -> Refs_Data.T) -> theory -> theory; (*from signature THEORY_DATA*)

     4.1 --- a/test/Tools/isac/Test_Isac_Short.thy	Sun Jan 17 13:16:25 2021 +0100
     4.2 +++ b/test/Tools/isac/Test_Isac_Short.thy	Sun Jan 17 15:25:27 2021 +0100
     4.3 @@ -287,6 +287,7 @@
     4.4    ... SAME ERROR HERE ON ISABELLE2012 AS IN ISAC ON ISABELLE2011*)
     4.5  
     4.6    ML_file "BridgeJEdit/parseC.sml"
     4.7 +  ML_file "BridgeJEdit/preliminary.sml"
     4.8  
     4.9    ML_file "Knowledge/delete.sml"
    4.10    ML_file "Knowledge/descript.sml"