1.1 --- a/src/Tools/isac/Build_Isac.thy	Tue Sep 10 16:13:28 2019 +0200
     1.2 +++ b/src/Tools/isac/Build_Isac.thy	Tue Sep 10 17:15:41 2019 +0200
     1.3 @@ -69,8 +69,7 @@
     1.4    ML_file "thy-hierarchy.sml" 
     1.5    ML_file "interface-xml.sml"
     1.6    ML_file interface.sml
     1.7 -          "BridgeLibisabelle/BridgeLibisabelle"
     1.8 -*)
     1.9 +*)        "BridgeLibisabelle/BridgeLibisabelle"
    1.10  
    1.11            "Knowledge/Build_Thydata" (*imports Isac.thy etc*)
    1.12  

     2.1 --- a/src/Tools/isac/Knowledge/Build_Thydata.thy	Tue Sep 10 16:13:28 2019 +0200
     2.2 +++ b/src/Tools/isac/Knowledge/Build_Thydata.thy	Tue Sep 10 17:15:41 2019 +0200
     2.3 @@ -65,14 +65,38 @@
     2.4    and "IsacScripts" is determined in KEStore.thy.
     2.5  \<close>
     2.6  ML \<open>
     2.7 -val thydata_list = []
     2.8 -(*//--------- outcomment "Exception- Size raised" during rm libisabelle ----------------------\\* )
     2.9 +val thydata_list =
    2.10    collect_part       "IsacKnowledge" knowledge_parent knowthys' @
    2.11    (map (collect_isab "Isabelle") rlsthmsNOTisac) @
    2.12    collect_part       "IsacScripts" proglang_parent progthys'
    2.13  : (Celem.theID * Celem.thydata) list
    2.14 -( *\\--------- outcomment "Exception- Size raised" during rm libisabelle ----------------------//*)
    2.15  \<close>
    2.16 +ML \<open>
    2.17 +map Rule.theory2thyID knowthys'
    2.18 +\<close> ML \<open>
    2.19 +Rule.theory2thyID knowledge_parent
    2.20 +\<close> text \<open>
    2.21 +  collect_part       "IsacKnowledge" knowledge_parent knowthys'
    2.22 +\<close> ML \<open>
    2.23 +"~~~~~ fun collect_part , args:"; val (part, parent, thys) = ("IsacKnowledge", knowledge_parent, knowthys');
    2.24 +\<close> ML \<open>
    2.25 +    val xxx = (flat (map (collect_thms part) thys))
    2.26 +\<close> ML \<open> (*isa*)
    2.27 +length thys = 32;
    2.28 +length xxx = 471
    2.29 +\<close> text \<open>
    2.30 +     (collect_rlss part (KEStore_Elems.get_rlss parent) thys)
    2.31 +\<close> text \<open>
    2.32 +"~~~~~ fun collect_rlss , args:"; val (part, rlss, thys) = (part, (KEStore_Elems.get_rlss parent), thys);
    2.33 +\<close> text \<open>
    2.34 +(* Build_Thydata.thy in jedit leads to "Exception- Size raised" <<<=============================== 
    2.35 +   =============================== but batch process =============================================
    2.36 +     ~~$ ./bin/isabelle build -o browser_info -v -b Isac
    2.37 +   =============================== works =========================================================
    2.38 +*)
    2.39 +KEStore_Elems.get_rlss parent
    2.40 +\<close>
    2.41 +
    2.42  setup \<open>KEStore_Elems.add_thes (map (fn (a, b) => (b, a)) thydata_list)\<close>
    2.43  
    2.44  section \<open>interface for dialog-authoring\<close>