1.1 --- a/src/Tools/isac/BridgeJEdit/Calculation.thy	Mon Mar 15 10:49:53 2021 +0100
     1.2 +++ b/src/Tools/isac/BridgeJEdit/Calculation.thy	Thu Mar 18 13:56:45 2021 +0100
     1.3 @@ -8,7 +8,7 @@
     1.4  theory Calculation
     1.5  imports
     1.6  (**) "~~/src/Tools/isac/Knowledge/Build_Thydata"   (*remove after devel.of BridgeJEdit*)
     1.7 -(** )"~~/src/Tools/isac/MathEngine/MathEngine"  ( *activate after devel.of BridgeJEdit*)
     1.8 +(**)"~~/src/Tools/isac/MathEngine/MathEngine"
     1.9  (**) "HOL-SPARK.SPARK"                             (*remove after devel.of BridgeJEdit*)
    1.10  keywords
    1.11  (*WAS "Example" :: thy_load ("str")  ..in Isabelle2020*)
    1.12 @@ -123,14 +123,14 @@
    1.13  (**)
    1.14  val _ =                                                  
    1.15    Outer_Syntax.command \<^command_keyword>\<open>Example\<close> "start a Calculation from a Formalise-file"
    1.16 -    (Resources.provide_parse_files (Command_Span.extensions [""]) -- Parse.parname
    1.17 +    (Resources.provide_parse_file -- Parse.parname
    1.18        >> (Toplevel.theory o           (*vvvvvvvvvvvvvvvvvvvv--- HACK makes test independent from session Isac*)
    1.19          (Preliminary.load_formalisation @{theory Biegelinie} ParseC.formalisation)) );
    1.20  (**)
    1.21  \<close> ML \<open>
    1.22  (Toplevel.theory o (Preliminary.load_formalisation @{theory Biegelinie} ParseC.formalisation))
    1.23  :
    1.24 -  (theory -> Token.file list * theory) * (*_a*)Token.T ->
    1.25 +  (theory -> Token.file * theory) * string ->
    1.26      Toplevel.transition -> Toplevel.transition
    1.27  (*  ^^^^^^^^^^^^^^^^^^^    ^^^^^^^^^^^^^^^^^^^*)
    1.28  \<close> ML \<open>

     2.1 --- a/src/Tools/isac/BridgeJEdit/preliminary.sml	Mon Mar 15 10:49:53 2021 +0100
     2.2 +++ b/src/Tools/isac/BridgeJEdit/preliminary.sml	Thu Mar 18 13:56:45 2021 +0100
     2.3 @@ -11,7 +11,7 @@
     2.4    (* for keyword Example *)
     2.5    val store_and_show: theory -> Formalise.T list -> theory -> theory;
     2.6    val load_formalisation: theory -> (Fdl_Lexer.T list -> ParseC.form_model_refs * 'a) ->
     2.7 -    (theory -> Token.file list * theory) * 'c -> theory -> theory
     2.8 +    (theory -> Token.file * theory) * string -> theory -> theory
     2.9    
    2.10    (* for keyword Problem*)
    2.11  (**)val init_specify: ParseC.problem_headline -> theory -> theory(**)
    2.12 @@ -88,12 +88,12 @@
    2.13          thy'
    2.14    end;
    2.15  *)
    2.16 -fun load_formalisation HACKthy parse (files, _) thy =
    2.17 +fun load_formalisation HACKthy parse (get_file: theory -> Token.file * theory, _: string) thy =
    2.18    let
    2.19 -    val ([{lines, pos, ...}: Token.file], thy') = files thy;
    2.20 -    val formalise = lines
    2.21 +    val (file, thy') = get_file thy;
    2.22 +    val formalise = #lines file
    2.23        |> cat_lines 
    2.24 -      |> ParseC.tokenize_formalise pos
    2.25 +      |> ParseC.tokenize_formalise (#pos file)
    2.26        |> fst
    2.27        |> parse
    2.28        |> fst