(*
   note that using "ttree-support.sml' assumes that all of the 
   tactic_tree/src/ files have already been read into eXene 
*)
 
use "base.sml";
use "syntax.sml";
structure Fol = FolFUN();
use "theorem.sml";

use "fol.grm.sig";
use "fol.grm.sml";
use "fol.lex.sml";
use "pretty.sml"; 
use "fol-pretty.sml";
structure tables_n_tokens = folLrValsFun(structure Token = LrParser.Token);
structure L = fol_lex(structure Tokens = tables_n_tokens.Tokens);
structure P = JoinWithArg(structure ParserData = tables_n_tokens.ParserData
                        structure Lex = L
                        structure LrParser = LrParser);
structure DispFol = DispFolFUN (structure Pretty=Pretty and Fol=Fol);
use "parse_strings.sml";
use "tactics.sml";
open Tactics;

use "ttree-support.sml";
structure Interactive = InteractiveTT (structure TTS = FOL_TTree_Support);
fun create(t,d,l) = 
     Interactive.create(Sequent ([],FolParseString.read_formula t), d,l) ;	
val view = Interactive.view;
val extract_event = Interactive.extract_event; 
val extract_tactic_text = Interactive.extract_tactic_text; 
val extract_text = Interactive.extract_text; 
val tactic_ref = FOL_TTree_Support.tactic_ref; 				      
use "test_formulas.sml"; 




