test/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml
changeset 59897 8cba439d0454
parent 59890 ba0757da0dc8
child 59898 68883c046963
     1.1 --- a/test/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml	Tue Apr 21 11:28:20 2020 +0200
     1.2 +++ b/test/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml	Tue Apr 21 12:26:08 2020 +0200
     1.3 @@ -90,14 +90,14 @@
     1.4  "----------- search for data error in thes2file ------------------";
     1.5  "----------- search for data error in thes2file ------------------";
     1.6  val TESTdump = Unsynchronized.ref 
     1.7 -  ("path": filepath, ["ids"]: theID, []: pos, thydata2file, Store.Ptyp ("xxx", [], []): thydata Store.ptyp);
     1.8 +  ("path": filepath, ["ids"]: theID, []: pos, thydata2file, Store.Node ("xxx", [], []): thydata Store.node);
     1.9  
    1.10 -fun TESTthenode (pa:filepath) ids po wfn (Store.Ptyp (id, [n], ns)) TESTids = 
    1.11 +fun TESTthenode (pa:filepath) ids po wfn (Store.Node (id, [n], ns)) TESTids = 
    1.12      let val po' = lev_on po
    1.13      in 
    1.14        if (ids@[id]) = TESTids
    1.15        then
    1.16 -        (TESTdump := (pa, ids, po', wfn, (Store.Ptyp (id, [n], ns))); 
    1.17 +        (TESTdump := (pa, ids, po', wfn, (Store.Node (id, [n], ns))); 
    1.18            error "stopped before error, created TESTdump") (* this exn creates right signature*)
    1.19        else
    1.20          wfn pa po' (ids @ [id]) n; TESTthenodes pa (ids @ [id]) ((lev_dn po'): pos) wfn ns TESTids
    1.21 @@ -120,7 +120,7 @@
    1.22  handle _(* "stopped before error, created TESTdump" *) => ());
    1.23  ;
    1.24  (* /----- uncomment in case of "data error in thes2file" ----------------------------(*1*)-----\*)
    1.25 -val (pa, ids, po', wfn, (Store.Ptyp (id, [n], ns))) = ! TESTdump; 
    1.26 +val (pa, ids, po', wfn, (Store.Node (id, [n], ns))) = ! TESTdump; 
    1.27  ;
    1.28  "~~~~~ fun thydata2file, args:"; val ((xmldata:filepath), (pos:pos), (theID:theID), thydata) =
    1.29    (pa, po', (ids@[id]), n);
    1.30 @@ -361,7 +361,7 @@
    1.31  "~~~~~ fun MINIthes2file, args:"; val (path) = ("/tmp/");
    1.32  "~~~~~ and thenodes, args:"; val (pa, ids, po, wfn, (n::ns)) = 
    1.33    (path, [], [0], thydata2file, MINIthehier);
    1.34 -"~~~~~ fun thenode, args:"; val ((pa : filepath), ids, po, wfn, (Store.Ptyp (id, [n], ns))) = 
    1.35 +"~~~~~ fun thenode, args:"; val ((pa : filepath), ids, po, wfn, (Store.Node (id, [n], ns))) = 
    1.36    (pa, ids, po, wfn, n);
    1.37  val po' = lev_on po;
    1.38  (*wfn pa po' (ids @ [id]) n  -------------> writes xml to file; we want xml before written: *)