# HG changeset patch # User wenzelm # Date 1310154287 -7200 # Node ID 3c2c912af2ef7dd6014c5df11aa356b6050e02c2 # Parent 608d1b451f678c632fe0c48a4d96e88422df5540 moved Outer_Syntax.load_thy to Thy_Load.load_thy; tuned signatures; tuned module dependencies; diff -r 608d1b451f67 -r 3c2c912af2ef src/Pure/Isar/outer_syntax.ML --- a/src/Pure/Isar/outer_syntax.ML Fri Jul 08 20:27:09 2011 +0200 +++ b/src/Pure/Isar/outer_syntax.ML Fri Jul 08 21:44:47 2011 +0200 @@ -10,6 +10,7 @@ signature OUTER_SYNTAX = sig type outer_syntax + val is_markup: outer_syntax -> Thy_Output.markup -> string -> bool val get_syntax: unit -> (Scan.lexicon * Scan.lexicon) * outer_syntax val command: string -> string -> Keyword.T -> (Toplevel.transition -> Toplevel.transition) parser -> unit @@ -33,8 +34,10 @@ val process_file: Path.T -> theory -> theory type isar val isar: TextIO.instream -> bool -> isar + val prepare_span: outer_syntax -> Thy_Syntax.span -> Toplevel.transition * bool + val prepare_element: outer_syntax -> (Path.T option -> theory) -> Thy_Syntax.element -> + (Toplevel.transition * Toplevel.transition list) list val prepare_command: Position.T -> string -> Toplevel.transition - val load_thy: string -> (Path.T option -> theory) -> Position.T -> string -> theory * unit future end; structure Outer_Syntax: OUTER_SYNTAX = @@ -283,41 +286,5 @@ | _ => Toplevel.malformed pos not_singleton) end; - -(* load_thy *) - -fun load_thy name init pos text = - let - val (lexs, outer_syntax) = get_syntax (); - val time = ! Toplevel.timing; - - val _ = Present.init_theory name; - - val toks = Source.exhausted (Thy_Syntax.token_source lexs pos (Source.of_string text)); - val spans = Source.exhaust (Thy_Syntax.span_source toks); - val _ = List.app Thy_Syntax.report_span spans; (* FIXME ?? *) - val elements = - Source.exhaust (Thy_Syntax.element_source (Source.of_list spans)) - |> Par_List.map_name "Outer_Syntax.prepare_element" (prepare_element outer_syntax init) - |> flat; - - val _ = Present.theory_source name - (fn () => HTML.html_mode (implode o map Thy_Syntax.present_span) spans); - - val _ = if time then writeln ("\n**** Starting theory " ^ quote name ^ " ****") else (); - val (results, thy) = cond_timeit time "" (fn () => Toplevel.excursion elements); - val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else (); - - val present = - singleton (Future.cond_forks {name = "Outer_Syntax.present:" ^ name, group = NONE, - deps = map Future.task_of results, pri = 0}) - (fn () => - Thy_Output.present_thy (#1 lexs) Keyword.command_tags (is_markup outer_syntax) - (maps Future.join results) toks - |> Buffer.content - |> Present.theory_output name); - - in (thy, present) end; - end; diff -r 608d1b451f67 -r 3c2c912af2ef src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Fri Jul 08 20:27:09 2011 +0200 +++ b/src/Pure/ROOT.ML Fri Jul 08 21:44:47 2011 +0200 @@ -243,18 +243,18 @@ use "Isar/typedecl.ML"; (*toplevel transactions*) -use "Thy/thy_load.ML"; use "Isar/proof_node.ML"; use "Isar/toplevel.ML"; (*theory documents*) use "System/isabelle_system.ML"; -use "Thy/present.ML"; use "Thy/term_style.ML"; use "Thy/thy_output.ML"; use "Thy/thy_syntax.ML"; use "Isar/outer_syntax.ML"; use "PIDE/document.ML"; +use "Thy/present.ML"; +use "Thy/thy_load.ML"; use "Thy/thy_info.ML"; use "Thy/rail.ML"; diff -r 608d1b451f67 -r 3c2c912af2ef src/Pure/Thy/present.ML --- a/src/Pure/Thy/present.ML Fri Jul 08 20:27:09 2011 +0200 +++ b/src/Pure/Thy/present.ML Fri Jul 08 21:44:47 2011 +0200 @@ -461,7 +461,7 @@ val files_html = files |> map (fn (raw_path, loadit) => let - val path = Thy_Load.check_file dir raw_path; + val path = File.check_file (File.full_path dir raw_path); val base = Path.base path; val base_html = html_ext base; val _ = add_file (Path.append html_prefix base_html, diff -r 608d1b451f67 -r 3c2c912af2ef src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Fri Jul 08 20:27:09 2011 +0200 +++ b/src/Pure/Thy/thy_info.ML Fri Jul 08 21:44:47 2011 +0200 @@ -241,7 +241,7 @@ fun required_by _ [] = "" | required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")"; -fun load_thy initiators update_time deps text name parent_thys = +fun load_thy initiators update_time deps text name parents = let val _ = kill_thy name; val _ = Output.urgent_message ("Loading theory " ^ quote name ^ required_by " " initiators); @@ -250,11 +250,8 @@ val dir = Path.dir thy_path; val pos = Path.position thy_path; val (_, _, uses) = Thy_Header.read pos text; - fun init _ = - Thy_Load.begin_theory dir name imports parent_thys uses - |> Present.begin_theory update_time dir uses; - val (theory, present) = Outer_Syntax.load_thy name init pos text; + val (theory, present) = Thy_Load.load_thy update_time dir name imports uses pos text parents; fun commit () = update_thy deps theory; in (theory, present, commit) end; @@ -332,8 +329,8 @@ val dir = (case master of SOME dir => dir | NONE => Thy_Load.get_master_path ()); val _ = kill_thy name; val _ = use_thys_wrt dir imports; - val parent_thys = map (get_theory o base_name) imports; - in Thy_Load.begin_theory dir name imports parent_thys uses end; + val parents = map (get_theory o base_name) imports; + in Thy_Load.begin_theory dir name imports uses parents end; (* register theory *) diff -r 608d1b451f67 -r 3c2c912af2ef src/Pure/Thy/thy_load.ML --- a/src/Pure/Thy/thy_load.ML Fri Jul 08 20:27:09 2011 +0200 +++ b/src/Pure/Thy/thy_load.ML Fri Jul 08 21:44:47 2011 +0200 @@ -18,7 +18,10 @@ val all_current: theory -> bool val use_ml: Path.T -> unit val exec_ml: Path.T -> generic_theory -> generic_theory - val begin_theory: Path.T -> string -> string list -> theory list -> (Path.T * bool) list -> theory + val begin_theory: Path.T -> string -> string list -> (Path.T * bool) list -> + theory list -> theory + val load_thy: int -> Path.T -> string -> string list -> (Path.T * bool) list -> + Position.T -> string -> theory list -> theory * unit future val set_master_path: Path.T -> unit val get_master_path: unit -> Path.T end; @@ -149,15 +152,53 @@ fun exec_ml src_path = ML_Context.exec (fn () => use_ml src_path); -(* begin theory *) +(* load_thy *) -fun begin_theory dir name imports parents uses = +fun begin_theory dir name imports uses parents = Theory.begin_theory name parents |> put_deps dir imports |> fold (require o fst) uses |> fold (fn (path, true) => Context.theory_map (exec_ml path) o Theory.checkpoint | _ => I) uses |> Theory.checkpoint; +fun load_thy update_time dir name imports uses pos text parents = + let + val (lexs, outer_syntax) = Outer_Syntax.get_syntax (); + val time = ! Toplevel.timing; + + val _ = Present.init_theory name; + fun init _ = + begin_theory dir name imports uses parents + |> Present.begin_theory update_time dir uses; + + val toks = Source.exhausted (Thy_Syntax.token_source lexs pos (Source.of_string text)); + val spans = Source.exhaust (Thy_Syntax.span_source toks); + val _ = List.app Thy_Syntax.report_span spans; (* FIXME ?? *) + val elements = + Source.exhaust (Thy_Syntax.element_source (Source.of_list spans)) + |> Par_List.map_name "Outer_Syntax.prepare_element" + (Outer_Syntax.prepare_element outer_syntax init) + |> flat; + + val _ = Present.theory_source name + (fn () => HTML.html_mode (implode o map Thy_Syntax.present_span) spans); + + val _ = if time then writeln ("\n**** Starting theory " ^ quote name ^ " ****") else (); + val (results, thy) = cond_timeit time "" (fn () => Toplevel.excursion elements); + val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else (); + + val present = + singleton (Future.cond_forks {name = "Outer_Syntax.present:" ^ name, group = NONE, + deps = map Future.task_of results, pri = 0}) + (fn () => + Thy_Output.present_thy (#1 lexs) Keyword.command_tags + (Outer_Syntax.is_markup outer_syntax) + (maps Future.join results) toks + |> Buffer.content + |> Present.theory_output name); + + in (thy, present) end; + (* global master path *)