wneuper/isa: comparison src/Tools/isac/xmlsrc/thy-hierarchy.sml

equal deleted inserted replaced

-:1c76b4b60f52
+:356e0272d565
 ((flat o (map (collect_thy "IsacScripts"))) scri_thys) @
 ((flat o (map (collect_thy "IsacKnowledge"))) isac_thys)
 	 : (theID * thydata) list
 end;
-fun show_thes () = (writeln o format_pblIDl o (scan [])) (!thehier);
+fun show_thes () = (writeln o format_pblIDl o (scan [])) (! thehier);
 (***.create the xml-format for the hierarchy.***)
 (*.create the hierarchy from a list (generated automatically);
 thus, missing parents of list-elems are inserted
 (causing msgs '*** insert: not found');
 elemes already store_*d in some *.ML are NOT overwritten.*)
 fun the_hier th ([]: (theID * thydata) list) = th
-(* val (th, (theID, thydata)::ths) = (!thehier, collect_thydata ());
+(* val (th, (theID, thydata)::ths) = (! thehier, collect_thydata ());
 *)
 | the_hier th ((theID, thydata)::ths) =
 if can_insert theID th
 then let val th' = if exist_the theID th
 		       then (writeln ("*** insert: preserved "^strs2str theID);
 str2file (path ^ "thy_hierarchy.xml")
 	     ("<NODE>\n" ^
 	      "  <ID> theory hierarchy </ID>\n" ^
 	      "  <NO> 1 </NO>\n" ^
 	      "  <CONTENTREF> thy_ROOT </CONTENTREF>\n" ^
-	     (hierarchy_guh (!thehier)) ^
+	     (hierarchy_guh (! thehier)) ^
 	     "</NODE>");
 (**.create the xml-files for the theory-data from the hierarchy.**)
 fun thenode (pa:path) ids po wfn (Ptyp (id,[n],ns)) =
 let val po' = lev_on po
 in wfn pa po' (ids@[id]) n;
 thenodes pa (ids@[id]) ((lev_dn po'):pos) wfn ns end
 (* val (pa,   ids,            po,  wfn,            (n::ns)) =
-(path, []:string list, [0], thydata2file, (!thehier));
+(path, []:string list, [0], thydata2file, (! thehier));
 *)
 and thenodes _ _ _ _ [] = ()
 | thenodes pa ids po wfn (n::ns) = (thenode pa ids po wfn n;
 				 thenodes pa ids (lev_on po) wfn ns);
 (*..analoguous to 'fun mets2file'*)
 fun thes2file (p : path) =
-thenodes p [] [0] thydata2file (!thehier);
+thenodes p [] [0] thydata2file (! thehier);
 (***.store a single theory element in the hierarchy.***)
 (*.for mathauthors only, other html is added to xml exported from here.*)
 	val the = Html {guh = guh,
 			coursedesign = [],
 			mathauthors = mathauthors,
 			html = ""}
 in (*needs no (!check_guhs_unique) because guh is generated automatically*)
-	thehier := insrt theID the theID (!thehier) end;
+	thehier := insrt theID the theID (! thehier) end;
 fun store_thy thy (mathauthors : authors) =
 let val guh = thy2guh ["IsacKnowledge", theory2thyID thy]
 	val theID = guh2theID guh
 	val the = Html {guh = guh,
 			coursedesign = [],
 			mathauthors = mathauthors,
 			html = ""}
 in (*needs no (!check_guhs_unique) because guh is generated automatically*)
-	thehier := insrt theID the theID (!thehier) end;
+	thehier := insrt theID the theID (! thehier) end;
 fun store_thm thy (thmID : thmID, thm) (mathauthors : authors) =
 let val guh = thm2guh ("IsacKnowledge", theory2thyID thy) thmID
 	val theID = guh2theID guh
 	val the = Hthm {guh = guh,
 			coursedesign = [], (*done at xml exported from here*)
 			mathauthors=mathauthors,
 			thm = thm}
 in (*needs no (!check_guhs_unique) because guh is generated automatically*)
-	thehier := insrt theID the theID (!thehier) end;
+	thehier := insrt theID the theID (! thehier) end;
 fun store_rls thy rls (mathauthors : authors) =
 let val guh = rls2guh ("IsacKnowledge", theory2thyID thy)
 			  ((#id o rep_rls)  rls)
 	val theID = guh2theID guh
 	val the = Hrls {guh = guh,
 			coursedesign = [],
 			mathauthors = mathauthors,
 			thy_rls=(theory2thyID thy, rls)}
 in (*needs no (!check_guhs_unique) because guh is generated automatically*)
-	thehier := insrt theID the theID (!thehier) end;
+	thehier := insrt theID the theID (! thehier) end;
 fun store_cal thy cal (mathauthors : authors) =
 let val guh = cal2guh ("IsacKnowledge", theory2thyID thy)
 			  ("TODO store_cal")
 	val theID = guh2theID guh
 	val the = Hcal {guh = guh,
 			coursedesign = [],
 			mathauthors = mathauthors,
 			calc = cal}
 in (*needs no (!check_guhs_unique) because guh is generated automatically*)
-	thehier := insrt theID the theID (!thehier) end;
+	thehier := insrt theID the theID (! thehier) end;
 fun store_ord thy ord (mathauthors : authors) =
 let val guh = ord2guh ("IsacKnowledge", theory2thyID thy)
 			  ("TODO store_ord")
 	val theID = guh2theID guh
 	val the = Hord {guh = guh,
 			coursedesign = [],
 			mathauthors = mathauthors,
 			ord = ord}
 in (*needs no (!check_guhs_unique) because guh is generated automatically*)
-	thehier := insrt theID the theID (!thehier) end;
+	thehier := insrt theID the theID (! thehier) end;

branch	isac-update-Isa09-2
changeset 38060	356e0272d565
parent 38031	460c24a6a6ba
child 42400	dcacb8077a98