1.1 --- a/src/Tools/isac/Build_Isac.thy	Sun Jun 15 18:39:59 2014 +0200
     1.2 +++ b/src/Tools/isac/Build_Isac.thy	Thu Jun 19 07:40:46 2014 +0200
     1.3 @@ -77,8 +77,7 @@
     1.4  ML {* check_guhs_unique := false; *}
     1.5  ML {* writeln "**** isac kernel = math-engine + Knowledge complete ******" *}
     1.6  ML {* @{theory "Isac"} *}
     1.7 -ML {* CHECK_FILLPATS "at end of Build_Isac";
     1.8 -(*"CHECK_FILLPATS: diff_sin_chain exists, fillpat --> NOT empty !!!"*)*}
     1.9 +ML {* get_the ["IsacKnowledge", "Diff", "Theorems", "diff_sin_chain"] *}
    1.10  
    1.11  section {* State of approaching Isabelle by Isac *}
    1.12  text {* 

     2.1 --- a/src/Tools/isac/KEStore.thy	Sun Jun 15 18:39:59 2014 +0200
     2.2 +++ b/src/Tools/isac/KEStore.thy	Thu Jun 19 07:40:46 2014 +0200
     2.3 @@ -106,21 +106,7 @@
     2.4      );                                                              
     2.5    fun get_thes thy = Data.get thy
     2.6    fun add_thes thes thy = let
     2.7 -    fun add_the (thydata, theID) =
     2.8 -      if can_insert theID (Data.get thy) 
     2.9 -      then
    2.10 -        if exist_the theID (Data.get thy)
    2.11 -        then (writeln ("*** insert: preserved " ^ strs2str theID); (fn x => x))
    2.12 -        else insrt theID thydata theID
    2.13 -      else
    2.14 -        let
    2.15 -          val th' = fill_parents (Data.get thy) theID theID (*..*** insert: not found*)
    2.16 -          val th' = insrt theID thydata theID th'
    2.17 -        in merge_ptyps' th' end; (*...TODO improve efficiency:
    2.18 -          val ((exist, notexist) branch) = fill_parents ([], theID) (Data.get thy)
    2.19 -            (* fill_parents: can_insert (hd theID), then insert the branch built from there;
    2.20 -            fill_parents probably could generalise to the then-branch above *)
    2.21 -        in insrt_branch exist branch end  (*notexist is in branch*)*)
    2.22 +    fun add_the (thydata, theID) = add_thydata ([], theID) thydata
    2.23    in Data.map (fold add_the thes) thy end;
    2.24    fun insert_fillpats fis thy =
    2.25      let

     3.1 --- a/src/Tools/isac/Knowledge/Build_Thydata.thy	Sun Jun 15 18:39:59 2014 +0200
     3.2 +++ b/src/Tools/isac/Knowledge/Build_Thydata.thy	Thu Jun 19 07:40:46 2014 +0200
     3.3 @@ -94,7 +94,7 @@
     3.4  
     3.5  section {* interface for dialog-authoring *}
     3.6  
     3.7 -(*/========= inhibit exn WN130620 (1.4.1) below: fill thehier ==============\*)
     3.8 +(*/========= inhibit exn WN130620 (1.4.1) below: fill thehier ==============\
     3.9  setup {*
    3.10  KEStore_Elems.add_thes
    3.11    [make_thy @{theory "Diff"} ["Isabelle2011-->12"],
    3.12 @@ -118,7 +118,7 @@
    3.13    make_thm @{theory "Test"} "IsacKnowledge" ("radd_left_commute", prop_of @{thm radd_left_commute})
    3.14     ["Isabelle2011-->12"]]
    3.15  *}
    3.16 -(*\========= inhibit exn WN130620 (1.4.1) below: fill thehier ==============/*)
    3.17 +\========= inhibit exn WN130620 (1.4.1) below: fill thehier ==============/*)
    3.18  
    3.19  subsection {* Add error patterns *}
    3.20  subsubsection {* Error patterns for differentiation *}

     4.1 --- a/src/Tools/isac/calcelems.sml	Sun Jun 15 18:39:59 2014 +0200
     4.2 +++ b/src/Tools/isac/calcelems.sml	Thu Jun 19 07:40:46 2014 +0200
     4.3 @@ -1035,6 +1035,27 @@
     4.4          in merge_ptyps' th' end;
     4.5  in fold (add_the th) thes end
     4.6  
     4.7 +fun Html_default exist = (Html {guh = theID2guh exist, 
     4.8 +  coursedesign = ["isac team 2006"], mathauthors = [], html = ""})
     4.9 +
    4.10 +fun fill_parents (exist, [i]) thydata = Ptyp (i, [thydata], [])
    4.11 +  | fill_parents (exist, i :: is) thydata =
    4.12 +    Ptyp (i, [Html_default (exist @ [i])], [fill_parents (exist @ [i], is) thydata])
    4.13 +  | fill_parents _ _ = error "Html_default: avoid ML warning: Matches are not exhaustive"
    4.14 +
    4.15 +fun add_thydata (exist, is) thydata [] = [fill_parents (exist, is) thydata]
    4.16 +  | add_thydata (exist, [i]) data (pys as (py as Ptyp (key, _, _)) :: pyss) = 
    4.17 +    if i = key
    4.18 +    then pys (* preserve existing thydata *) 
    4.19 +    else py :: add_thydata (exist, [i]) data pyss
    4.20 +  | add_thydata (exist, iss as (i :: is)) data ((py as Ptyp (key, d, pys)) :: pyss) = 
    4.21 +    if i = key
    4.22 +    then       
    4.23 +      if length pys = 0
    4.24 +      then Ptyp (key, d, [fill_parents (exist @ [i], is) data]) :: pyss
    4.25 +      else Ptyp (key, d, add_thydata (exist @ [i], is) data pys) :: pyss
    4.26 +    else py :: add_thydata (exist, iss) data pyss
    4.27 +  | add_thydata _ _ _ = error "add_thydata: avoid ML warning: Matches are not exhaustive"
    4.28  
    4.29  fun update_hthm (Hthm {guh, coursedesign, mathauthors, thm, ...}) fillpats' =
    4.30    Hthm {guh = guh, coursedesign = coursedesign, mathauthors = mathauthors,