1.1 --- a/TODO.md	Mon May 03 09:36:47 2021 +0200
     1.2 +++ b/TODO.md	Fri May 07 13:23:24 2021 +0200
     1.3 @@ -39,8 +39,3 @@
     1.4  * WN: simplify const names like "is'_expanded": no need to imitate the escape of mixfix syntax;
     1.5  
     1.6  * WN: "fun pr_ord" is not required if used with @{make_string}, @{print}, @{print tracing};
     1.7 -
     1.8 -* WN: use File.read / File.write instead of low-level TextIO operations (not portable);
     1.9 -* WN: use Path.T (e.g. via Path.explode) for portability;
    1.10 -* WN: refrain from using global /tmp directory
    1.11 -  (e.g. see Isabelle_System.create_tmp_path / with_tmp_file / with_tmp_dir);

     2.1 --- a/src/Tools/isac/BridgeLibisabelle/BridgeLibisabelle.thy	Mon May 03 09:36:47 2021 +0200
     2.2 +++ b/src/Tools/isac/BridgeLibisabelle/BridgeLibisabelle.thy	Fri May 07 13:23:24 2021 +0200
     2.3 @@ -20,15 +20,5 @@
     2.4  ML \<open>
     2.5  \<close> ML \<open>
     2.6  \<close> ML \<open>
     2.7 -(*
     2.8 -  The only code kept for generation of XML (required by the deprecated Java-frontend)
     2.9 -  is called below.
    2.10 -  The hierarchies will still be required in addition to PIDE functionality.
    2.11 -*)
    2.12 -val path = "/home/wneuper/tmp/"; (*~/tmp/pbl/ and ~/tmp/met must be created manyally*)
    2.13 -\<close> text \<open>(* ATTENTION: outcomment before commits, because the directories must exist *)
    2.14 -Pbl_Met_Hierarchy.pbl_hierarchy2file (path ^ "pbl/");
    2.15 -Pbl_Met_Hierarchy.met_hierarchy2file (path ^ "met/");
    2.16 -\<close> ML \<open>
    2.17  \<close>
    2.18  end

     3.1 --- a/src/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml	Mon May 03 09:36:47 2021 +0200
     3.2 +++ b/src/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml	Fri May 07 13:23:24 2021 +0200
     3.3 @@ -12,12 +12,9 @@
     3.4    eqtype filepath
     3.5    eqtype filename
     3.6    type xml
     3.7 -  val pbl_hierarchy2file: filepath -> unit
     3.8 -  val met_hierarchy2file: filepath -> unit
     3.9 +  val pbl_hierarchy2file : filepath -> filepath * string
    3.10 +  val met_hierarchy2file : filepath -> filepath * string
    3.11    val update_metpair: theory -> MethodC.id -> Error_Pattern_Def.T list -> MethodC.T * MethodC.id
    3.12 -\<^isac_test>\<open>
    3.13 -  val str2file: filename -> string -> unit
    3.14 -\<close>
    3.15  end
    3.16  
    3.17  (**)
    3.18 @@ -68,6 +65,7 @@
    3.19  	    | nds i p (n::ns) = (nd i p n) ^ (nds i (Pos.lev_on p) ns);
    3.20    in nds j [0] h  : xml end;
    3.21  
    3.22 +(*
    3.23  fun str2file (fnm : filename) (str : string) =
    3.24    let val file = TextIO.openOut fnm
    3.25    in 
    3.26 @@ -75,17 +73,18 @@
    3.27      TextIO.flushOut file;
    3.28      TextIO.closeOut file
    3.29    end
    3.30 +*)
    3.31  fun pbl_hierarchy2file path = 
    3.32 -    str2file (path ^ "pbl_hierarchy.xml") 
    3.33 -	     ("<NODE>\n" ^
    3.34 +    (*str2file*) (path ^ "pbl_hierarchy.xml" : filepath,
    3.35 +	      "<NODE>\n" ^
    3.36  	      "  <ID> problem hierarchy </ID>\n" ^
    3.37  	      "  <NO> 1 </NO>\n" ^
    3.38  	      "  <CONTENTREF> pbl_ROOT </CONTENTREF>\n" ^
    3.39  	     (hierarchy_pbl (get_ptyps ())) ^
    3.40  	     "</NODE>");
    3.41  fun met_hierarchy2file path = 
    3.42 -    str2file (path ^ "met_hierarchy.xml") 
    3.43 -	     ("<NODE>\n" ^
    3.44 +    (*str2file*) (path ^ "met_hierarchy.xml" : filepath,
    3.45 +	      "<NODE>\n" ^
    3.46  	      "  <ID> method hierarchy </ID>\n" ^
    3.47  	      "  <NO> 1 </NO>\n" ^
    3.48  	      "  <CONTENTREF> met_ROOT </CONTENTREF>\n" ^

     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/test/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml	Fri May 07 13:23:24 2021 +0200
     4.3 @@ -0,0 +1,30 @@
     4.4 +(* Title:  "Interpret/lucas-interpreter.sml"
     4.5 +   Author: Walther Neuper
     4.6 +   (c) due to copyright terms
     4.7 +*)
     4.8 +
     4.9 +"-----------------------------------------------------------------------------------------------";
    4.10 +"table of contents -----------------------------------------------------------------------------";
    4.11 +"-----------------------------------------------------------------------------------------------";
    4.12 +"----------- fun pbl_hierarchy2file ------------------------------------------------------------";
    4.13 +"----------- fun met_hierarchy2file ------------------------------------------------------------";
    4.14 +"-----------------------------------------------------------------------------------------------";
    4.15 +"-----------------------------------------------------------------------------------------------";
    4.16 +"-----------------------------------------------------------------------------------------------";
    4.17 +
    4.18 +
    4.19 +"----------- fun pbl_hierarchy2file ------------------------------------------------------------";
    4.20 +"----------- fun pbl_hierarchy2file ------------------------------------------------------------";
    4.21 +"----------- fun pbl_hierarchy2file ------------------------------------------------------------";
    4.22 +if Pbl_Met_Hierarchy.pbl_hierarchy2file "dummy/path/" =
    4.23 +   ("dummy/path/pbl_hierarchy.xml",
    4.24 +    "<NODE>\n  <ID> problem hierarchy </ID>\n  <NO> 1 </NO>\n  <CONTENTREF> pbl_ROOT </CONTENTREF>\n  <NODE>\n    <ID> empty_probl_id </ID>\n    <NO> 1 </NO>\n    <CONTENTREF> pbl_empty </CONTENTREF>\n  </NODE>\n  <NODE>\n    <ID> simplification </ID>\n    <NO> 2 </NO>\n    <CONTENTREF> pbl_simp </CONTENTREF>\n    <NODE>\n      <ID> polynomial </ID>\n      <NO> 1 </NO>\n      <CONTENTREF> pbl_simp_poly </CONTENTREF>\n    </NODE>\n    <NODE>\n      <ID> rational </ID>\n      <NO> 2 </NO>\n      <CONTENTREF> pbl_simp_rat </CONTENTREF>\n      <NODE>\n        <ID> partial_fraction </ID>\n        <NO> 1 </NO>\n        <CONTENTREF> pbl_simp_rat_partfrac </CONTENTREF>\n      </NODE>\n    </NODE>\n  </NODE>\n  <NODE>\n    <ID> vereinfachen </ID>\n    <NO> 3 </NO>\n    <CONTENTREF> pbl_vereinfache </CONTENTREF>\n    <NODE>\n      <ID> polynom </ID>\n      <NO> 1 </NO>\n      <CONTENTREF> pbl_vereinf_poly </CONTENTREF>\n      <NODE>\n        <ID> plus_minus </ID>\n        <NO> 1 </NO>\n        <CONTENTREF> pbl_vereinf_poly_minus </CONTENTREF>\n      </NODE>\n      <NODE>\n        <ID> klammer </ID>\n        <NO> 2 </NO>\n        <CONTENTREF> pbl_vereinf_poly_klammer </CONTENTREF>\n      </NODE>\n      <NODE>\n        <ID> binom_klammer </ID>\n        <NO> 3 </NO>\n        <CONTENTREF> pbl_vereinf_poly_klammer_mal </CONTENTREF>\n      </NODE>\n    </NODE>\n  </NODE>\n  <NODE>\n    <ID> probe </ID>\n    <NO> 4 </NO>\n    <CONTENTREF> pbl_probe </CONTENTREF>\n    <NODE>\n      <ID> polynom </ID>\n      <NO> 1 </NO>\n      <CONTENTREF> pbl_probe_poly </CONTENTREF>\n    </NODE>\n    <NODE>\n      <ID> bruch </ID>\n      <NO> 2 </NO>\n      <CONTENTREF> pbl_probe_bruch </CONTENTREF>\n    </NODE>\n  </NODE>\n  <NODE>\n    <ID> equation </ID>\n    <NO> 5 </NO>\n    <CONTENTREF> pbl_equ </CONTENTREF>\n    <NODE>\n      <ID> univariate </ID>\n      <NO> 1 </NO>\n      <CONTENTREF> pbl_equ_univ </CONTENTREF>\n      <NODE>\n        <ID> rootX </ID>\n        <NO> 1 </NO>\n        <CONTENTREF> pbl_equ_univ_root </CONTENTREF>\n        <NODE>\n          <ID> sq </ID>\n          <NO> 1 </NO>\n          <CONTENTREF> pbl_equ_univ_root_sq </CONTENTREF>\n          <NODE>\n            <ID> rat </ID>\n            <NO> 1 </NO>\n            <CONTENTREF> pbl_equ_univ_root_sq_rat </CONTENTREF>\n          </NODE>\n        </NODE>\n        <NODE>\n          <ID> normalise </ID>\n          <NO> 2 </NO>\n          <CONTENTREF> pbl_equ_univ_root_norm </CONTENTREF>\n        </NODE>\n      </NODE>\n      <NODE>\n        <ID> LINEAR </ID>\n        <NO> 2 </NO>\n        <CONTENTREF> pbl_equ_univ_lin </CONTENTREF>\n      </NODE>\n      <NODE>\n        <ID> rational </ID>\n        <NO> 3 </NO>\n        <CONTENTREF> pbl_equ_univ_rat </CONTENTREF>\n      </NODE>\n      <NODE>\n        <ID> polynomial </ID>\n        <NO> 4 </NO>\n        <CONTENTREF> pbl_equ_univ_poly </CONTENTREF>\n        <NODE>\n          <ID> degree_0 </ID>\n          <NO> 1 </NO>\n          <CONTENTREF> pbl_equ_univ_poly_deg0 </CONTENTREF>\n        </NODE>\n        <NODE>\n          <ID> degree_1 </ID>\n          <NO> 2 </NO>\n          <CONTENTREF> pbl_equ_univ_poly_deg1 </CONTENTREF>\n        </NODE>\n        <NODE>\n          <ID> degree_2 </ID>\n          <NO> 3 </NO>\n          <CONTENTREF> pbl_equ_univ_poly_deg2 </CONTENTREF>\n          <NODE>\n            <ID> sq_only </ID>\n            <NO> 1 </NO>\n            <CONTENTREF> pbl_equ_univ_poly_deg2_sqonly </CONTENTREF>\n          </NODE>\n          <NODE>\n            <ID> bdv_only </ID>\n            <NO> 2 </NO>\n            <CONTENTREF> pbl_equ_univ_poly_deg2_bdvonly </CONTENTREF>\n          </NODE>\n          <NODE>\n            <ID> pqFormula </ID>\n            <NO> 3 </NO>\n            <CONTENTREF> pbl_equ_univ_poly_deg2_pq </CONTENTREF>\n          </NODE>\n          <NODE>\n            <ID> abcFormula </ID>\n            <NO> 4 </NO>\n            <CONTENTREF> pbl_equ_univ_poly_deg2_abc </CONTENTREF>\n          </NODE>\n        </NODE>\n        <NODE>\n          <ID> degree_3 </ID>\n          <NO> 4 </NO>\n          <CONTENTREF> pbl_equ_univ_poly_deg3 </CONTENTREF>\n        </NODE>\n        <NODE>\n          <ID> degree_4 </ID>\n          <NO> 5 </NO>\n          <CONTENTREF> pbl_equ_univ_poly_deg4 </CONTENTREF>\n        </NODE>\n        <NODE>\n          <ID> normalise </ID>\n          <NO> 6 </NO>\n          <CONTENTREF> pbl_equ_univ_poly_norm </CONTENTREF>\n        </NODE>\n      </NODE>\n      <NODE>\n        <ID> expanded </ID>\n        <NO> 5 </NO>\n        <CONTENTREF> pbl_equ_univ_expand </CONTENTREF>\n        <NODE>\n          <ID> degree_2 </ID>\n          <NO> 1 </NO>\n          <CONTENTREF> pbl_equ_univ_expand_deg2 </CONTENTREF>\n        </NODE>\n      </NODE>\n      <NODE>\n        <ID> logarithmic </ID>\n        <NO> 6 </NO>\n        <CONTENTREF> pbl_test_equ_univ_log </CONTENTREF>\n      </NODE>\n    </NODE>\n    <NODE>\n      <ID> makeFunctionTo </ID>\n      <NO> 2 </NO>\n      <CONTENTREF> pbl_equ_fromfun </CONTENTREF>\n    </NODE>\n    <NODE>\n      <ID> diophantine </ID>\n      <NO> 3 </NO>\n      <CONTENTREF> pbl_equ_dio </CONTENTREF>\n    </NODE>\n  </NODE>\n  <NODE>\n    <ID> function </ID>\n    <NO> 6 </NO>\n    <CONTENTREF> pbl_fun </CONTENTREF>\n    <NODE>\n      <ID> derivative_of </ID>\n      <NO> 1 </NO>\n      <CONTENTREF> pbl_fun_deriv </CONTENTREF>\n      <NODE>\n        <ID> named </ID>\n        <NO> 1 </NO>\n        <CONTENTREF> pbl_fun_deriv_nam </CONTENTREF>\n      </NODE>\n    </NODE>\n    <NODE>\n      <ID> integrate </ID>\n      <NO> 2 </NO>\n      <CONTENTREF> pbl_fun_integ </CONTENTREF>\n      <NODE>\n        <ID> named </ID>\n        <NO> 1 </NO>\n        <CONTENTREF> pbl_fun_integ_nam </CONTENTREF>\n      </NODE>\n    </NODE>\n    <NODE>\n      <ID> maximum_of </ID>\n      <NO> 3 </NO>\n      <CONTENTREF> pbl_fun_max </CONTENTREF>\n      <NODE>\n        <ID> on_interval </ID>\n        <NO> 1 </NO>\n        <CONTENTREF> pbl_fun_max_interv </CONTENTREF>\n      </NODE>\n    </NODE>\n    <NODE>\n      <ID> make </ID>\n      <NO> 4 </NO>\n      <CONTENTREF> pbl_fun_make </CONTENTREF>\n      <NODE>\n        <ID> by_explicit </ID>\n        <NO> 1 </NO>\n        <CONTENTREF> pbl_fun_max_expl </CONTENTREF>\n      </NODE>\n      <NODE>\n        <ID> by_new_variable </ID>\n        <NO> 2 </NO>\n        <CONTENTREF> pbl_fun_max_newvar </CONTENTREF>\n      </NODE>\n    </NODE>\n  </NODE>\n  <NODE>\n    <ID> system </ID>\n    <NO> 7 </NO>\n    <CONTENTREF> pbl_equsys </CONTENTREF>\n    <NODE>\n      <ID> LINEAR </ID>\n      <NO> 1 </NO>\n      <CONTENTREF> pbl_equsys_lin </CONTENTREF>\n      <NODE>\n        <ID> 2x2 </ID>\n        <NO> 1 </NO>\n        <CONTENTREF> pbl_equsys_lin_2x2 </CONTENTREF>\n        <NODE>\n          <ID> triangular </ID>\n          <NO> 1 </NO>\n          <CONTENTREF> pbl_equsys_lin_2x2_tri </CONTENTREF>\n        </NODE>\n        <NODE>\n          <ID> normalise </ID>\n          <NO> 2 </NO>\n          <CONTENTREF> pbl_equsys_lin_2x2_norm </CONTENTREF>\n        </NODE>\n      </NODE>\n      <NODE>\n        <ID> 3x3 </ID>\n        <NO> 2 </NO>\n        <CONTENTREF> pbl_equsys_lin_3x3 </CONTENTREF>\n      </NODE>\n      <NODE>\n        <ID> 4x4 </ID>\n        <NO> 3 </NO>\n        <CONTENTREF> pbl_equsys_lin_4x4 </CONTENTREF>\n        <NODE>\n          <ID> triangular </ID>\n          <NO> 1 </NO>\n          <CONTENTREF> pbl_equsys_lin_4x4_tri </CONTENTREF>\n        </NODE>\n        <NODE>\n          <ID> normalise </ID>\n          <NO> 2 </NO>\n          <CONTENTREF> pbl_equsys_lin_4x4_norm </CONTENTREF>\n        </NODE>\n      </NODE>\n    </NODE>\n  </NODE>\n  <NODE>\n    <ID> Biegelinien </ID>\n    <NO> 8 </NO>\n    <CONTENTREF> pbl_bieg </CONTENTREF>\n    <NODE>\n      <ID> MomentBestimmte </ID>\n      <NO> 1 </NO>\n      <CONTENTREF> pbl_bieg_mom </CONTENTREF>\n    </NODE>\n    <NODE>\n      <ID> MomentGegebene </ID>\n      <NO> 2 </NO>\n      <CONTENTREF> pbl_bieg_momg </CONTENTREF>\n    </NODE>\n    <NODE>\n      <ID> einfache </ID>\n      <NO> 3 </NO>\n      <CONTENTREF> pbl_bieg_einf </CONTENTREF>\n    </NODE>\n    <NODE>\n      <ID> QuerkraftUndMomentBestimmte </ID>\n      <NO> 4 </NO>\n      <CONTENTREF> pbl_bieg_momquer </CONTENTREF>\n    </NODE>\n    <NODE>\n      <ID> vonBelastungZu </ID>\n      <NO> 5 </NO>\n      <CONTENTREF> pbl_bieg_vonq </CONTENTREF>\n    </NODE>\n    <NODE>\n      <ID> setzeRandbedingungen </ID>\n      <NO> 6 </NO>\n      <CONTENTREF> pbl_bieg_randbed </CONTENTREF>\n    </NODE>\n  </NODE>\n  <NODE>\n    <ID> Berechnung </ID>\n    <NO> 9 </NO>\n    <CONTENTREF> pbl_algein </CONTENTREF>\n    <NODE>\n      <ID> numerischSymbolische </ID>\n      <NO> 1 </NO>\n      <CONTENTREF> pbl_algein_numsym </CONTENTREF>\n    </NODE>\n  </NODE>\n  <NODE>\n    <ID> Programming </ID>\n    <NO> 10 </NO>\n    <CONTENTREF> pbl_Programming </CONTENTREF>\n    <NODE>\n      <ID> SORT </ID>\n      <NO> 1 </NO>\n      <CONTENTREF> pbl_Prog_sort </CONTENTREF>\n      <NODE>\n        <ID> insertion </ID>\n        <NO> 1 </NO>\n        <CONTENTREF> pbl_Prog_sort_ins </CONTENTREF>\n      </NODE>\n    </NODE>\n  </NODE>\n  <NODE>\n    <ID> test </ID>\n    <NO> 11 </NO>\n    <CONTENTREF> pbl_test </CONTENTREF>\n    <NODE>\n      <ID> equation </ID>\n      <NO> 1 </NO>\n      <CONTENTREF> pbl_test_equ </CONTENTREF>\n      <NODE>\n        <ID> univariate </ID>\n        <NO> 1 </NO>\n        <CONTENTREF> pbl_test_uni </CONTENTREF>\n        <NODE>\n          <ID> LINEAR </ID>\n          <NO> 1 </NO>\n          <CONTENTREF> pbl_test_uni_lin </CONTENTREF>\n        </NODE>\n        <NODE>\n          <ID> plain_square </ID>\n          <NO> 2 </NO>\n          <CONTENTREF> pbl_test_uni_plain2 </CONTENTREF>\n        </NODE>\n        <NODE>\n          <ID> polynomial </ID>\n          <NO> 3 </NO>\n          <CONTENTREF> pbl_test_uni_poly </CONTENTREF>\n          <NODE>\n            <ID> degree_two </ID>\n            <NO> 1 </NO>\n            <CONTENTREF> pbl_test_uni_poly_deg2 </CONTENTREF>\n            <NODE>\n              <ID> pq_formula </ID>\n              <NO> 1 </NO>\n              <CONTENTREF> pbl_test_uni_poly_deg2_pq </CONTENTREF>\n            </NODE>\n            <NODE>\n              <ID> abc_formula </ID>\n              <NO> 2 </NO>\n              <CONTENTREF> pbl_test_uni_poly_deg2_abc </CONTENTREF>\n            </NODE>\n          </NODE>\n        </NODE>\n        <NODE>\n          <ID> squareroot </ID>\n          <NO> 4 </NO>\n          <CONTENTREF> pbl_test_uni_root </CONTENTREF>\n        </NODE>\n        <NODE>\n          <ID> normalise </ID>\n          <NO> 5 </NO>\n          <CONTENTREF> pbl_test_uni_norm </CONTENTREF>\n        </NODE>\n        <NODE>\n          <ID> sqroot-test </ID>\n          <NO> 6 </NO>\n          <CONTENTREF> pbl_test_uni_roottest </CONTENTREF>\n        </NODE>\n      </NODE>\n    </NODE>\n    <NODE>\n      <ID> inttype </ID>\n      <NO> 2 </NO>\n      <CONTENTREF> pbl_test_intsimp </CONTENTREF>\n    </NODE>\n    <NODE>\n      <ID> refine </ID>\n      <NO> 3 </NO>\n      <CONTENTREF> pbl_test_refine </CONTENTREF>\n      <NODE>\n        <ID> pbla </ID>\n        <NO> 1 </NO>\n        <CONTENTREF> pbl_pbla </CONTENTREF>\n        <NODE>\n          <ID> pbla1 </ID>\n          <NO> 1 </NO>\n          <CONTENTREF> pbl_pbla1 </CONTENTREF>\n        </NODE>\n        <NODE>\n          <ID> pbla2 </ID>\n          <NO> 2 </NO>\n          <CONTENTREF> pbl_pbla2 </CONTENTREF>\n          <NODE>\n            <ID> pbla2x </ID>\n            <NO> 1 </NO>\n            <CONTENTREF> pbl_pbla2x </CONTENTREF>\n          </NODE>\n          <NODE>\n            <ID> pbla2y </ID>\n            <NO> 2 </NO>\n            <CONTENTREF> pbl_pbla2y </CONTENTREF>\n          </NODE>\n          <NODE>\n            <ID> pbla2z </ID>\n            <NO> 3 </NO>\n            <CONTENTREF> pbl_pbla2z </CONTENTREF>\n          </NODE>\n        </NODE>\n        <NODE>\n          <ID> pbla3 </ID>\n          <NO> 3 </NO>\n          <CONTENTREF> pbl_pbla3 </CONTENTREF>\n        </NODE>\n      </NODE>\n    </NODE>\n    <NODE>\n      <ID> calculate </ID>\n      <NO> 4 </NO>\n      <CONTENTREF> pbl_ttest_calc </CONTENTREF>\n    </NODE>\n  </NODE>\n  <NODE>\n    <ID> tool </ID>\n    <NO> 12 </NO>\n    <CONTENTREF> pbl_tool </CONTENTREF>\n    <NODE>\n      <ID> find_values </ID>\n      <NO> 1 </NO>\n      <CONTENTREF> pbl_tool_findvals </CONTENTREF>\n    </NODE>\n  </NODE>\n  <NODE>\n    <ID> SignalProcessing </ID>\n    <NO> 13 </NO>\n    <CONTENTREF> pbl_SP </CONTENTREF>\n    <NODE>\n      <ID> Z_Transform </ID>\n      <NO> 1 </NO>\n      <CONTENTREF> pbl_SP_Ztrans </CONTENTREF>\n      <NODE>\n        <ID> Inverse </ID>\n        <NO> 1 </NO>\n        <CONTENTREF> pbl_SP_Ztrans_inv </CONTENTREF>\n      </NODE>\n    </NODE>\n  </NODE>\n</NODE>")
    4.25 +then () else error "pbl_hierarchy2file CHANGED: has a Problem_Pattern been updated?"
    4.26 +
    4.27 +"----------- fun met_hierarchy2file ------------------------------------------------------------";
    4.28 +"----------- fun met_hierarchy2file ------------------------------------------------------------";
    4.29 +"----------- fun met_hierarchy2file ------------------------------------------------------------";
    4.30 +if Pbl_Met_Hierarchy.met_hierarchy2file "dummy/path/" =
    4.31 +   ("dummy/path/met_hierarchy.xml",
    4.32 +    "<NODE>\n  <ID> method hierarchy </ID>\n  <NO> 1 </NO>\n  <CONTENTREF> met_ROOT </CONTENTREF>\n  <NODE>\n    <ID> empty_meth_id </ID>\n    <NO> 1 </NO>\n    <CONTENTREF> met_empty </CONTENTREF>\n  </NODE>\n  <NODE>\n    <ID> simplification </ID>\n    <NO> 2 </NO>\n    <CONTENTREF> met_tsimp </CONTENTREF>\n    <NODE>\n      <ID> for_polynomials </ID>\n      <NO> 1 </NO>\n      <CONTENTREF> met_simp_poly </CONTENTREF>\n      <NODE>\n        <ID> with_minus </ID>\n        <NO> 1 </NO>\n        <CONTENTREF> met_simp_poly_minus </CONTENTREF>\n      </NODE>\n      <NODE>\n        <ID> with_parentheses </ID>\n        <NO> 2 </NO>\n        <CONTENTREF> met_simp_poly_parenth </CONTENTREF>\n      </NODE>\n      <NODE>\n        <ID> with_parentheses_mult </ID>\n        <NO> 3 </NO>\n        <CONTENTREF> met_simp_poly_parenth_mult </CONTENTREF>\n      </NODE>\n    </NODE>\n    <NODE>\n      <ID> of_rationals </ID>\n      <NO> 2 </NO>\n      <CONTENTREF> met_simp_rat </CONTENTREF>\n      <NODE>\n        <ID> to_partial_fraction </ID>\n        <NO> 1 </NO>\n        <CONTENTREF> met_partial_fraction </CONTENTREF>\n      </NODE>\n    </NODE>\n  </NODE>\n  <NODE>\n    <ID> probe </ID>\n    <NO> 3 </NO>\n    <CONTENTREF> met_probe </CONTENTREF>\n    <NODE>\n      <ID> fuer_polynom </ID>\n      <NO> 1 </NO>\n      <CONTENTREF> met_probe_poly </CONTENTREF>\n    </NODE>\n    <NODE>\n      <ID> fuer_bruch </ID>\n      <NO> 2 </NO>\n      <CONTENTREF> met_probe_bruch </CONTENTREF>\n    </NODE>\n  </NODE>\n  <NODE>\n    <ID> Equation </ID>\n    <NO> 4 </NO>\n    <CONTENTREF> met_equ </CONTENTREF>\n    <NODE>\n      <ID> solve_log </ID>\n      <NO> 1 </NO>\n      <CONTENTREF> met_equ_log </CONTENTREF>\n    </NODE>\n    <NODE>\n      <ID> fromFunction </ID>\n      <NO> 2 </NO>\n      <CONTENTREF> met_equ_fromfun </CONTENTREF>\n    </NODE>\n  </NODE>\n  <NODE>\n    <ID> RootEq </ID>\n    <NO> 5 </NO>\n    <CONTENTREF> met_rooteq </CONTENTREF>\n    <NODE>\n      <ID> norm_sq_root_equation </ID>\n      <NO> 1 </NO>\n      <CONTENTREF> met_rooteq_norm </CONTENTREF>\n    </NODE>\n    <NODE>\n      <ID> solve_sq_root_equation </ID>\n      <NO> 2 </NO>\n      <CONTENTREF> met_rooteq_sq </CONTENTREF>\n    </NODE>\n    <NODE>\n      <ID> solve_right_sq_root_equation </ID>\n      <NO> 3 </NO>\n      <CONTENTREF> met_rooteq_sq_right </CONTENTREF>\n    </NODE>\n    <NODE>\n      <ID> solve_left_sq_root_equation </ID>\n      <NO> 4 </NO>\n      <CONTENTREF> met_rooteq_sq_left </CONTENTREF>\n    </NODE>\n  </NODE>\n  <NODE>\n    <ID> LinEq </ID>\n    <NO> 6 </NO>\n    <CONTENTREF> met_eqlin </CONTENTREF>\n    <NODE>\n      <ID> solve_lineq_equation </ID>\n      <NO> 1 </NO>\n      <CONTENTREF> met_eq_lin </CONTENTREF>\n    </NODE>\n  </NODE>\n  <NODE>\n    <ID> RatEq </ID>\n    <NO> 7 </NO>\n    <CONTENTREF> met_rateq </CONTENTREF>\n    <NODE>\n      <ID> solve_rat_equation </ID>\n      <NO> 1 </NO>\n      <CONTENTREF> met_rat_eq </CONTENTREF>\n    </NODE>\n  </NODE>\n  <NODE>\n    <ID> RootRatEq </ID>\n    <NO> 8 </NO>\n    <CONTENTREF> met_rootrateq </CONTENTREF>\n    <NODE>\n      <ID> elim_rootrat_equation </ID>\n      <NO> 1 </NO>\n      <CONTENTREF> met_rootrateq_elim </CONTENTREF>\n    </NODE>\n  </NODE>\n  <NODE>\n    <ID> PolyEq </ID>\n    <NO> 9 </NO>\n    <CONTENTREF> met_polyeq </CONTENTREF>\n    <NODE>\n      <ID> normalise_poly </ID>\n      <NO> 1 </NO>\n      <CONTENTREF> met_polyeq_norm </CONTENTREF>\n    </NODE>\n    <NODE>\n      <ID> solve_d0_polyeq_equation </ID>\n      <NO> 2 </NO>\n      <CONTENTREF> met_polyeq_d0 </CONTENTREF>\n    </NODE>\n    <NODE>\n      <ID> solve_d1_polyeq_equation </ID>\n      <NO> 3 </NO>\n      <CONTENTREF> met_polyeq_d1 </CONTENTREF>\n    </NODE>\n    <NODE>\n      <ID> solve_d2_polyeq_equation </ID>\n      <NO> 4 </NO>\n      <CONTENTREF> met_polyeq_d22 </CONTENTREF>\n    </NODE>\n    <NODE>\n      <ID> solve_d2_polyeq_bdvonly_equation </ID>\n      <NO> 5 </NO>\n      <CONTENTREF> met_polyeq_d2_bdvonly </CONTENTREF>\n    </NODE>\n    <NODE>\n      <ID> solve_d2_polyeq_sqonly_equation </ID>\n      <NO> 6 </NO>\n      <CONTENTREF> met_polyeq_d2_sqonly </CONTENTREF>\n    </NODE>\n    <NODE>\n      <ID> solve_d2_polyeq_pq_equation </ID>\n      <NO> 7 </NO>\n      <CONTENTREF> met_polyeq_d2_pq </CONTENTREF>\n    </NODE>\n    <NODE>\n      <ID> solve_d2_polyeq_abc_equation </ID>\n      <NO> 8 </NO>\n      <CONTENTREF> met_polyeq_d2_abc </CONTENTREF>\n    </NODE>\n    <NODE>\n      <ID> solve_d3_polyeq_equation </ID>\n      <NO> 9 </NO>\n      <CONTENTREF> met_polyeq_d3 </CONTENTREF>\n    </NODE>\n    <NODE>\n      <ID> complete_square </ID>\n      <NO> 10 </NO>\n      <CONTENTREF> met_polyeq_complsq </CONTENTREF>\n    </NODE>\n  </NODE>\n  <NODE>\n    <ID> diff </ID>\n    <NO> 10 </NO>\n    <CONTENTREF> met_diff </CONTENTREF>\n    <NODE>\n      <ID> differentiate_on_R </ID>\n      <NO> 1 </NO>\n      <CONTENTREF> met_diff_onR </CONTENTREF>\n    </NODE>\n    <NODE>\n      <ID> diff_simpl </ID>\n      <NO> 2 </NO>\n      <CONTENTREF> met_diff_simpl </CONTENTREF>\n    </NODE>\n    <NODE>\n      <ID> differentiate_equality </ID>\n      <NO> 3 </NO>\n      <CONTENTREF> met_diff_equ </CONTENTREF>\n    </NODE>\n    <NODE>\n      <ID> after_simplification </ID>\n      <NO> 4 </NO>\n      <CONTENTREF> met_diff_after_simp </CONTENTREF>\n    </NODE>\n    <NODE>\n      <ID> integration </ID>\n      <NO> 5 </NO>\n      <CONTENTREF> met_diffint </CONTENTREF>\n      <NODE>\n        <ID> named </ID>\n        <NO> 1 </NO>\n        <CONTENTREF> met_diffint_named </CONTENTREF>\n      </NODE>\n      <NODE>\n        <ID> test </ID>\n        <NO> 2 </NO>\n        <CONTENTREF> met_testint </CONTENTREF>\n      </NODE>\n    </NODE>\n  </NODE>\n  <NODE>\n    <ID> EqSystem </ID>\n    <NO> 11 </NO>\n    <CONTENTREF> met_eqsys </CONTENTREF>\n    <NODE>\n      <ID> top_down_substitution </ID>\n      <NO> 1 </NO>\n      <CONTENTREF> met_eqsys_topdown </CONTENTREF>\n      <NODE>\n        <ID> 2x2 </ID>\n        <NO> 1 </NO>\n        <CONTENTREF> met_eqsys_topdown_2x2 </CONTENTREF>\n      </NODE>\n      <NODE>\n        <ID> 4x4 </ID>\n        <NO> 2 </NO>\n        <CONTENTREF> met_eqsys_topdown_4x4 </CONTENTREF>\n      </NODE>\n    </NODE>\n    <NODE>\n      <ID> normalise </ID>\n      <NO> 2 </NO>\n      <CONTENTREF> met_eqsys_norm </CONTENTREF>\n      <NODE>\n        <ID> 2x2 </ID>\n        <NO> 1 </NO>\n        <CONTENTREF> met_eqsys_norm_2x2 </CONTENTREF>\n      </NODE>\n      <NODE>\n        <ID> 4x4 </ID>\n        <NO> 2 </NO>\n        <CONTENTREF> met_eqsys_norm_4x4 </CONTENTREF>\n      </NODE>\n    </NODE>\n  </NODE>\n  <NODE>\n    <ID> IntegrierenUndKonstanteBestimmen </ID>\n    <NO> 12 </NO>\n    <CONTENTREF> met_biege </CONTENTREF>\n    <NODE>\n      <ID> 2xIntegrieren </ID>\n      <NO> 1 </NO>\n      <CONTENTREF> met_biege_intconst_2 </CONTENTREF>\n    </NODE>\n    <NODE>\n      <ID> 4x4System </ID>\n      <NO> 2 </NO>\n      <CONTENTREF> met_biege_intconst_4 </CONTENTREF>\n    </NODE>\n    <NODE>\n      <ID> 1xIntegrieren </ID>\n      <NO> 3 </NO>\n      <CONTENTREF> met_biege_intconst_1 </CONTENTREF>\n    </NODE>\n  </NODE>\n  <NODE>\n    <ID> IntegrierenUndKonstanteBestimmen2 </ID>\n    <NO> 13 </NO>\n    <CONTENTREF> met_biege_2 </CONTENTREF>\n  </NODE>\n  <NODE>\n    <ID> Biegelinien </ID>\n    <NO> 14 </NO>\n    <CONTENTREF> met_biege2 </CONTENTREF>\n    <NODE>\n      <ID> ausBelastung </ID>\n      <NO> 1 </NO>\n      <CONTENTREF> met_biege_ausbelast </CONTENTREF>\n    </NODE>\n    <NODE>\n      <ID> setzeRandbedingungenEin </ID>\n      <NO> 2 </NO>\n      <CONTENTREF> met_biege_setzrand </CONTENTREF>\n    </NODE>\n  </NODE>\n  <NODE>\n    <ID> Berechnung </ID>\n    <NO> 15 </NO>\n    <CONTENTREF> met_algein </CONTENTREF>\n    <NODE>\n      <ID> erstNumerisch </ID>\n      <NO> 1 </NO>\n      <CONTENTREF> met_algein_numsym_1num </CONTENTREF>\n    </NODE>\n    <NODE>\n      <ID> erstSymbolisch </ID>\n      <NO> 2 </NO>\n      <CONTENTREF> met_algein_symnum </CONTENTREF>\n    </NODE>\n  </NODE>\n  <NODE>\n    <ID> Programming </ID>\n    <NO> 16 </NO>\n    <CONTENTREF> met_Programming </CONTENTREF>\n    <NODE>\n      <ID> SORT </ID>\n      <NO> 1 </NO>\n      <CONTENTREF> met_Prog_sort </CONTENTREF>\n      <NODE>\n        <ID> insertion </ID>\n        <NO> 1 </NO>\n        <CONTENTREF> met_Prog_sort_ins </CONTENTREF>\n      </NODE>\n      <NODE>\n        <ID> insertion_steps </ID>\n        <NO> 2 </NO>\n        <CONTENTREF> met_Prog_sort_ins_steps </CONTENTREF>\n      </NODE>\n    </NODE>\n  </NODE>\n  <NODE>\n    <ID> Test </ID>\n    <NO> 17 </NO>\n    <CONTENTREF> met_test </CONTENTREF>\n    <NODE>\n      <ID> solve_linear </ID>\n      <NO> 1 </NO>\n      <CONTENTREF> met_test_solvelin </CONTENTREF>\n    </NODE>\n    <NODE>\n      <ID> sqrt-equ-test </ID>\n      <NO> 2 </NO>\n      <CONTENTREF> met_test_sqrt </CONTENTREF>\n    </NODE>\n    <NODE>\n      <ID> squ-equ-test-subpbl1 </ID>\n      <NO> 3 </NO>\n      <CONTENTREF> met_test_squ_sub </CONTENTREF>\n    </NODE>\n    <NODE>\n      <ID> square_equation1 </ID>\n      <NO> 4 </NO>\n      <CONTENTREF> met_test_eq1 </CONTENTREF>\n    </NODE>\n    <NODE>\n      <ID> square_equation2 </ID>\n      <NO> 5 </NO>\n      <CONTENTREF> met_test_squ2 </CONTENTREF>\n    </NODE>\n    <NODE>\n      <ID> square_equation </ID>\n      <NO> 6 </NO>\n      <CONTENTREF> met_test_squeq </CONTENTREF>\n    </NODE>\n    <NODE>\n      <ID> solve_plain_square </ID>\n      <NO> 7 </NO>\n      <CONTENTREF> met_test_eq_plain </CONTENTREF>\n    </NODE>\n    <NODE>\n      <ID> norm_univar_equation </ID>\n      <NO> 8 </NO>\n      <CONTENTREF> met_test_norm_univ </CONTENTREF>\n    </NODE>\n    <NODE>\n      <ID> intsimp </ID>\n      <NO> 9 </NO>\n      <CONTENTREF> met_test_intsimp </CONTENTREF>\n    </NODE>\n    <NODE>\n      <ID> solve_diophant </ID>\n      <NO> 10 </NO>\n      <CONTENTREF> met_test_diophant </CONTENTREF>\n    </NODE>\n    <NODE>\n      <ID> test_calculate </ID>\n      <NO> 11 </NO>\n      <CONTENTREF> met_testcal </CONTENTREF>\n    </NODE>\n  </NODE>\n  <NODE>\n    <ID> DiffApp </ID>\n    <NO> 18 </NO>\n    <CONTENTREF> met_diffapp </CONTENTREF>\n    <NODE>\n      <ID> max_by_calculus </ID>\n      <NO> 1 </NO>\n      <CONTENTREF> met_diffapp_max </CONTENTREF>\n    </NODE>\n    <NODE>\n      <ID> make_fun_by_new_variable </ID>\n      <NO> 2 </NO>\n      <CONTENTREF> met_diffapp_funnew </CONTENTREF>\n    </NODE>\n    <NODE>\n      <ID> make_fun_by_explicit </ID>\n      <NO> 3 </NO>\n      <CONTENTREF> met_diffapp_funexp </CONTENTREF>\n    </NODE>\n    <NODE>\n      <ID> max_on_interval_by_calculus </ID>\n      <NO> 4 </NO>\n      <CONTENTREF> met_diffapp_max_oninterval </CONTENTREF>\n    </NODE>\n    <NODE>\n      <ID> find_values </ID>\n      <NO> 5 </NO>\n      <CONTENTREF> met_diffapp_findvals </CONTENTREF>\n    </NODE>\n  </NODE>\n  <NODE>\n    <ID> SignalProcessing </ID>\n    <NO> 19 </NO>\n    <CONTENTREF> met_SP </CONTENTREF>\n    <NODE>\n      <ID> Z_Transform </ID>\n      <NO> 1 </NO>\n      <CONTENTREF> met_SP_Ztrans </CONTENTREF>\n      <NODE>\n        <ID> Inverse </ID>\n        <NO> 1 </NO>\n        <CONTENTREF> met_SP_Ztrans_inv </CONTENTREF>\n      </NODE>\n      <NODE>\n        <ID> Inverse_sub </ID>\n        <NO> 2 </NO>\n        <CONTENTREF> met_SP_Ztrans_inv_sub </CONTENTREF>\n      </NODE>\n    </NODE>\n  </NODE>\n</NODE>")
    4.33 +then () else error "met_hierarchy2file CHANGED: has a Method been updated?"

     5.1 --- a/test/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml	Mon May 03 09:36:47 2021 +0200
     5.2 +++ b/test/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml	Fri May 07 13:23:24 2021 +0200
     5.3 @@ -119,11 +119,15 @@
     5.4  "----------- ..CONTINUED: we adapt some required MINIfunctions ---";
     5.5  fun MINIget_the (theID : Thy_Write.theID) = Store.get MINIthehier theID theID (*see ptyps.sml*)
     5.6  fun MINIthy_hierarchy2file (path:Pbl_Met_Hierarchy.filepath) = 
     5.7 -  Pbl_Met_Hierarchy.str2file (path ^ "thy_hierarchy.xml") 
     5.8 -    ("<NODE>\n" ^
     5.9 +  (*Pbl_Met_Hierarchy.str2file*) (path ^ "thy_hierarchy.xml",
    5.10 +    "<NODE>\n" ^
    5.11      "  <ID> theory hierarchy </ID>\n" ^
    5.12      "  <NO> 1 </NO>\n" ^
    5.13      "  <CONTENTREF> thy_ROOT </CONTENTREF>\n" ^
    5.14      (Thy_Hierarchy.hierarchy_guh MINIthehier) ^
    5.15      "</NODE>");
    5.16 +if MINIthy_hierarchy2file "xxx/" =
    5.17 +   ("xxx/thy_hierarchy.xml",
    5.18 +    "<NODE>\n  <ID> theory hierarchy </ID>\n  <NO> 1 </NO>\n  <CONTENTREF> thy_ROOT </CONTENTREF>\n  <NODE>\n    <ID> IsacKnowledge </ID>\n    <NO> 1 </NO>\n    <CONTENTREF> thy_isac_IsacKnowledge-part </CONTENTREF>\n    <NODE>\n      <ID> Test_Build_Thydata </ID>\n      <NO> 1 </NO>\n      <CONTENTREF> thy_isac_Test_Build_Thydata </CONTENTREF>\n      <NODE>\n        <ID> Theorems </ID>\n        <NO> 1 </NO>\n        <CONTENTREF> thy_isac_Test_Build_Thydata-Theorems </CONTENTREF>\n        <NODE>\n          <ID> thm111 </ID>\n          <NO> 1 </NO>\n          <CONTENTREF> thy_isac_Test_Build_Thydata-thm-thm111 </CONTENTREF>\n        </NODE>\n        <NODE>\n          <ID> thm222 </ID>\n          <NO> 2 </NO>\n          <CONTENTREF> thy_isac_Test_Build_Thydata-thm-thm222 </CONTENTREF>\n        </NODE>\n      </NODE>\n      <NODE>\n        <ID> Rulesets </ID>\n        <NO> 2 </NO>\n        <CONTENTREF> thy_isac_Test_Build_Thydata-Rulesets </CONTENTREF>\n        <NODE>\n          <ID> rls111 </ID>\n          <NO> 1 </NO>\n          <CONTENTREF> thy_isac_Test_Build_Thydata-rls-rls111 </CONTENTREF>\n        </NODE>\n        <NODE>\n          <ID> rls222 </ID>\n          <NO> 2 </NO>\n          <CONTENTREF> thy_isac_Test_Build_Thydata-rls-rls222 </CONTENTREF>\n        </NODE>\n      </NODE>\n    </NODE>\n  </NODE>\n  <NODE>\n    <ID> Isabelle </ID>\n    <NO> 2 </NO>\n    <CONTENTREF> thy_isab_Isabelle-part </CONTENTREF>\n    <NODE>\n      <ID> HOL </ID>\n      <NO> 1 </NO>\n      <CONTENTREF> thy_isab_HOL </CONTENTREF>\n      <NODE>\n        <ID> Theorems </ID>\n        <NO> 1 </NO>\n        <CONTENTREF> thy_isab_HOL-Theorems </CONTENTREF>\n        <NODE>\n          <ID> refl </ID>\n          <NO> 1 </NO>\n          <CONTENTREF> thy_isab_HOL-thm-refl </CONTENTREF>\n        </NODE>\n      </NODE>\n    </NODE>\n    <NODE>\n      <ID> Fun </ID>\n      <NO> 2 </NO>\n      <CONTENTREF> thy_isab_Fun </CONTENTREF>\n      <NODE>\n        <ID> Theorems </ID>\n        <NO> 1 </NO>\n        <CONTENTREF> thy_isab_Fun-Theorems </CONTENTREF>\n        <NODE>\n          <ID> o_def </ID>\n          <NO> 1 </NO>\n          <CONTENTREF> thy_isab_Fun-thm-o_def </CONTENTREF>\n        </NODE>\n      </NODE>\n    </NODE>\n  </NODE>\n  <NODE>\n    <ID> IsacScripts </ID>\n    <NO> 3 </NO>\n    <CONTENTREF> thy_scri_IsacScripts-part </CONTENTREF>\n    <NODE>\n      <ID> Test_Build_Thydata </ID>\n      <NO> 1 </NO>\n      <CONTENTREF> thy_scri_Test_Build_Thydata </CONTENTREF>\n      <NODE>\n        <ID> Theorems </ID>\n        <NO> 1 </NO>\n        <CONTENTREF> thy_scri_Test_Build_Thydata-Theorems </CONTENTREF>\n        <NODE>\n          <ID> thm111 </ID>\n          <NO> 1 </NO>\n          <CONTENTREF> thy_scri_Test_Build_Thydata-thm-thm111 </CONTENTREF>\n        </NODE>\n        <NODE>\n          <ID> thm222 </ID>\n          <NO> 2 </NO>\n          <CONTENTREF> thy_scri_Test_Build_Thydata-thm-thm222 </CONTENTREF>\n        </NODE>\n      </NODE>\n    </NODE>\n  </NODE>\n</NODE>")
    5.19 +then () else error "MINIthy_hierarchy2file CHANGED";
    5.20  

     6.1 --- a/test/Tools/isac/Test_Isac_Short.thy	Mon May 03 09:36:47 2021 +0200
     6.2 +++ b/test/Tools/isac/Test_Isac_Short.thy	Fri May 07 13:23:24 2021 +0200
     6.3 @@ -263,6 +263,7 @@
     6.4  
     6.5    ML_file "BridgeLibisabelle/thy-present.sml"
     6.6    ML_file "BridgeLibisabelle/mathml.sml"           (*part.*)
     6.7 +  ML_file "BridgeLibisabelle/pbl-met-hierarchy.sml"
     6.8    ML_file "BridgeLibisabelle/thy-hierarchy.sml"
     6.9    ML_file "BridgeLibisabelle/interface-xml.sml"     (*TODO after 2009-2*)
    6.10    ML_file "BridgeLibisabelle/interface.sml"