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: *)