1.1 --- a/NEWS Mon May 31 19:36:13 2010 +0200
1.2 +++ b/NEWS Mon May 31 21:06:57 2010 +0200
1.3 @@ -503,9 +503,12 @@
1.4 OuterLex ~> Token
1.5 OuterParse ~> Parse
1.6 OuterSyntax ~> Outer_Syntax
1.7 + PrintMode ~> Print_Mode
1.8 SpecParse ~> Parse_Spec
1.9 + ThyInfo ~> Thy_Info
1.10 + ThyLoad ~> Thy_Load
1.11 + ThyOutput ~> Thy_Output
1.12 TypeInfer ~> Type_Infer
1.13 - PrintMode ~> Print_Mode
1.14
1.15 Note that "open Legacy" simplifies porting of sources, but forgetting
1.16 to remove it again will complicate porting again in the future.
2.1 --- a/doc-src/Classes/Thy/document/Classes.tex Mon May 31 19:36:13 2010 +0200
2.2 +++ b/doc-src/Classes/Thy/document/Classes.tex Mon May 31 21:06:57 2010 +0200
2.3 @@ -792,8 +792,7 @@
2.4 \isamarkuptrue%
2.5 %
2.6 \begin{isamarkuptext}%
2.7 -Isabelle locales support a concept of local definitions
2.8 - in locales:%
2.9 +Isabelle locales are targets which support local definitions:%
2.10 \end{isamarkuptext}%
2.11 \isamarkuptrue%
2.12 %
3.1 --- a/doc-src/IsarImplementation/Thy/Integration.thy Mon May 31 19:36:13 2010 +0200
3.2 +++ b/doc-src/IsarImplementation/Thy/Integration.thy Mon May 31 21:06:57 2010 +0200
3.3 @@ -368,13 +368,13 @@
3.4 @{index_ML theory: "string -> theory"} \\
3.5 @{index_ML use_thy: "string -> unit"} \\
3.6 @{index_ML use_thys: "string list -> unit"} \\
3.7 - @{index_ML ThyInfo.touch_thy: "string -> unit"} \\
3.8 - @{index_ML ThyInfo.remove_thy: "string -> unit"} \\[1ex]
3.9 - @{index_ML ThyInfo.begin_theory}@{verbatim ": ... -> bool -> theory"} \\
3.10 - @{index_ML ThyInfo.end_theory: "theory -> unit"} \\
3.11 - @{index_ML ThyInfo.register_theory: "theory -> unit"} \\[1ex]
3.12 + @{index_ML Thy_Info.touch_thy: "string -> unit"} \\
3.13 + @{index_ML Thy_Info.remove_thy: "string -> unit"} \\[1ex]
3.14 + @{index_ML Thy_Info.begin_theory}@{verbatim ": ... -> bool -> theory"} \\
3.15 + @{index_ML Thy_Info.end_theory: "theory -> unit"} \\
3.16 + @{index_ML Thy_Info.register_theory: "theory -> unit"} \\[1ex]
3.17 @{verbatim "datatype action = Update | Outdate | Remove"} \\
3.18 - @{index_ML ThyInfo.add_hook: "(ThyInfo.action -> string -> unit) -> unit"} \\
3.19 + @{index_ML Thy_Info.add_hook: "(Thy_Info.action -> string -> unit) -> unit"} \\
3.20 \end{mldecls}
3.21
3.22 \begin{description}
3.23 @@ -395,24 +395,24 @@
3.24 intrinsic parallelism can be exploited by the system, to speedup
3.25 loading.
3.26
3.27 - \item @{ML ThyInfo.touch_thy}~@{text A} performs and @{text outdate} action
3.28 + \item @{ML Thy_Info.touch_thy}~@{text A} performs and @{text outdate} action
3.29 on theory @{text A} and all descendants.
3.30
3.31 - \item @{ML ThyInfo.remove_thy}~@{text A} deletes theory @{text A} and all
3.32 + \item @{ML Thy_Info.remove_thy}~@{text A} deletes theory @{text A} and all
3.33 descendants from the theory database.
3.34
3.35 - \item @{ML ThyInfo.begin_theory} is the basic operation behind a
3.36 + \item @{ML Thy_Info.begin_theory} is the basic operation behind a
3.37 @{text \<THEORY>} header declaration. This {\ML} function is
3.38 normally not invoked directly.
3.39
3.40 - \item @{ML ThyInfo.end_theory} concludes the loading of a theory
3.41 + \item @{ML Thy_Info.end_theory} concludes the loading of a theory
3.42 proper and stores the result in the theory database.
3.43
3.44 - \item @{ML ThyInfo.register_theory}~@{text "text thy"} registers an
3.45 + \item @{ML Thy_Info.register_theory}~@{text "text thy"} registers an
3.46 existing theory value with the theory loader database. There is no
3.47 management of associated sources.
3.48
3.49 - \item @{ML "ThyInfo.add_hook"}~@{text f} registers function @{text
3.50 + \item @{ML "Thy_Info.add_hook"}~@{text f} registers function @{text
3.51 f} as a hook for theory database actions. The function will be
3.52 invoked with the action and theory name being involved; thus derived
3.53 actions may be performed in associated system components, e.g.\
4.1 --- a/doc-src/IsarImplementation/Thy/document/Integration.tex Mon May 31 19:36:13 2010 +0200
4.2 +++ b/doc-src/IsarImplementation/Thy/document/Integration.tex Mon May 31 21:06:57 2010 +0200
4.3 @@ -440,13 +440,13 @@
4.4 \indexdef{}{ML}{theory}\verb|theory: string -> theory| \\
4.5 \indexdef{}{ML}{use\_thy}\verb|use_thy: string -> unit| \\
4.6 \indexdef{}{ML}{use\_thys}\verb|use_thys: string list -> unit| \\
4.7 - \indexdef{}{ML}{ThyInfo.touch\_thy}\verb|ThyInfo.touch_thy: string -> unit| \\
4.8 - \indexdef{}{ML}{ThyInfo.remove\_thy}\verb|ThyInfo.remove_thy: string -> unit| \\[1ex]
4.9 - \indexdef{}{ML}{ThyInfo.begin\_theory}\verb|ThyInfo.begin_theory|\verb|: ... -> bool -> theory| \\
4.10 - \indexdef{}{ML}{ThyInfo.end\_theory}\verb|ThyInfo.end_theory: theory -> unit| \\
4.11 - \indexdef{}{ML}{ThyInfo.register\_theory}\verb|ThyInfo.register_theory: theory -> unit| \\[1ex]
4.12 + \indexdef{}{ML}{Thy\_Info.touch\_thy}\verb|Thy_Info.touch_thy: string -> unit| \\
4.13 + \indexdef{}{ML}{Thy\_Info.remove\_thy}\verb|Thy_Info.remove_thy: string -> unit| \\[1ex]
4.14 + \indexdef{}{ML}{Thy\_Info.begin\_theory}\verb|Thy_Info.begin_theory|\verb|: ... -> bool -> theory| \\
4.15 + \indexdef{}{ML}{Thy\_Info.end\_theory}\verb|Thy_Info.end_theory: theory -> unit| \\
4.16 + \indexdef{}{ML}{Thy\_Info.register\_theory}\verb|Thy_Info.register_theory: theory -> unit| \\[1ex]
4.17 \verb|datatype action = Update |\verb,|,\verb| Outdate |\verb,|,\verb| Remove| \\
4.18 - \indexdef{}{ML}{ThyInfo.add\_hook}\verb|ThyInfo.add_hook: (ThyInfo.action -> string -> unit) -> unit| \\
4.19 + \indexdef{}{ML}{Thy\_Info.add\_hook}\verb|Thy_Info.add_hook: (Thy_Info.action -> string -> unit) -> unit| \\
4.20 \end{mldecls}
4.21
4.22 \begin{description}
4.23 @@ -466,24 +466,24 @@
4.24 intrinsic parallelism can be exploited by the system, to speedup
4.25 loading.
4.26
4.27 - \item \verb|ThyInfo.touch_thy|~\isa{A} performs and \isa{outdate} action
4.28 + \item \verb|Thy_Info.touch_thy|~\isa{A} performs and \isa{outdate} action
4.29 on theory \isa{A} and all descendants.
4.30
4.31 - \item \verb|ThyInfo.remove_thy|~\isa{A} deletes theory \isa{A} and all
4.32 + \item \verb|Thy_Info.remove_thy|~\isa{A} deletes theory \isa{A} and all
4.33 descendants from the theory database.
4.34
4.35 - \item \verb|ThyInfo.begin_theory| is the basic operation behind a
4.36 + \item \verb|Thy_Info.begin_theory| is the basic operation behind a
4.37 \isa{{\isasymTHEORY}} header declaration. This {\ML} function is
4.38 normally not invoked directly.
4.39
4.40 - \item \verb|ThyInfo.end_theory| concludes the loading of a theory
4.41 + \item \verb|Thy_Info.end_theory| concludes the loading of a theory
4.42 proper and stores the result in the theory database.
4.43
4.44 - \item \verb|ThyInfo.register_theory|~\isa{text\ thy} registers an
4.45 + \item \verb|Thy_Info.register_theory|~\isa{text\ thy} registers an
4.46 existing theory value with the theory loader database. There is no
4.47 management of associated sources.
4.48
4.49 - \item \verb|ThyInfo.add_hook|~\isa{f} registers function \isa{f} as a hook for theory database actions. The function will be
4.50 + \item \verb|Thy_Info.add_hook|~\isa{f} registers function \isa{f} as a hook for theory database actions. The function will be
4.51 invoked with the action and theory name being involved; thus derived
4.52 actions may be performed in associated system components, e.g.\
4.53 maintaining the state of an editor for the theory sources.
5.1 --- a/doc-src/IsarRef/Thy/ROOT-HOLCF.ML Mon May 31 19:36:13 2010 +0200
5.2 +++ b/doc-src/IsarRef/Thy/ROOT-HOLCF.ML Mon May 31 21:06:57 2010 +0200
5.3 @@ -1,4 +1,4 @@
5.4 -Unsynchronized.set ThyOutput.source;
5.5 +Unsynchronized.set Thy_Output.source;
5.6 use "../../antiquote_setup.ML";
5.7
5.8 use_thy "HOLCF_Specific";
6.1 --- a/doc-src/IsarRef/Thy/ROOT-ZF.ML Mon May 31 19:36:13 2010 +0200
6.2 +++ b/doc-src/IsarRef/Thy/ROOT-ZF.ML Mon May 31 21:06:57 2010 +0200
6.3 @@ -1,4 +1,4 @@
6.4 -Unsynchronized.set ThyOutput.source;
6.5 +Unsynchronized.set Thy_Output.source;
6.6 use "../../antiquote_setup.ML";
6.7
6.8 use_thy "ZF_Specific";
7.1 --- a/doc-src/IsarRef/Thy/ROOT.ML Mon May 31 19:36:13 2010 +0200
7.2 +++ b/doc-src/IsarRef/Thy/ROOT.ML Mon May 31 21:06:57 2010 +0200
7.3 @@ -1,5 +1,5 @@
7.4 Unsynchronized.set quick_and_dirty;
7.5 -Unsynchronized.set ThyOutput.source;
7.6 +Unsynchronized.set Thy_Output.source;
7.7 use "../../antiquote_setup.ML";
7.8
7.9 use_thys [
8.1 --- a/doc-src/Main/Docs/Main_Doc.thy Mon May 31 19:36:13 2010 +0200
8.2 +++ b/doc-src/Main/Docs/Main_Doc.thy Mon May 31 21:06:57 2010 +0200
8.3 @@ -9,10 +9,10 @@
8.4 else error "term_type_only: type mismatch";
8.5 Syntax.pretty_typ ctxt T)
8.6
8.7 -val _ = ThyOutput.antiquotation "term_type_only" (Args.term -- Args.typ_abbrev)
8.8 +val _ = Thy_Output.antiquotation "term_type_only" (Args.term -- Args.typ_abbrev)
8.9 (fn {source, context, ...} => fn arg =>
8.10 - ThyOutput.output
8.11 - (ThyOutput.maybe_pretty_source (pretty_term_type_only context) source [arg]));
8.12 + Thy_Output.output
8.13 + (Thy_Output.maybe_pretty_source (pretty_term_type_only context) source [arg]));
8.14 *}
8.15 (*>*)
8.16 text{*
9.1 --- a/doc-src/System/Thy/ROOT.ML Mon May 31 19:36:13 2010 +0200
9.2 +++ b/doc-src/System/Thy/ROOT.ML Mon May 31 21:06:57 2010 +0200
9.3 @@ -1,4 +1,4 @@
9.4 -Unsynchronized.set ThyOutput.source;
9.5 +Unsynchronized.set Thy_Output.source;
9.6 use "../../antiquote_setup.ML";
9.7
9.8 use_thys ["Basics", "Interfaces", "Presentation", "Misc"];
10.1 --- a/doc-src/TutorialI/Rules/Primes.thy Mon May 31 19:36:13 2010 +0200
10.2 +++ b/doc-src/TutorialI/Rules/Primes.thy Mon May 31 21:06:57 2010 +0200
10.3 @@ -10,7 +10,7 @@
10.4
10.5
10.6 ML "Pretty.margin_default := 64"
10.7 -ML "ThyOutput.indent := 5" (*that is, Doc/TutorialI/settings.ML*)
10.8 +ML "Thy_Output.indent := 5" (*that is, Doc/TutorialI/settings.ML*)
10.9
10.10
10.11 text {*Now in Basic.thy!
11.1 --- a/doc-src/TutorialI/Types/Numbers.thy Mon May 31 19:36:13 2010 +0200
11.2 +++ b/doc-src/TutorialI/Types/Numbers.thy Mon May 31 21:06:57 2010 +0200
11.3 @@ -3,7 +3,7 @@
11.4 begin
11.5
11.6 ML "Pretty.margin_default := 64"
11.7 -ML "ThyOutput.indent := 0" (*we don't want 5 for listing theorems*)
11.8 +ML "Thy_Output.indent := 0" (*we don't want 5 for listing theorems*)
11.9
11.10 text{*
11.11
12.1 --- a/doc-src/TutorialI/Types/document/Numbers.tex Mon May 31 19:36:13 2010 +0200
12.2 +++ b/doc-src/TutorialI/Types/document/Numbers.tex Mon May 31 21:06:57 2010 +0200
12.3 @@ -28,7 +28,7 @@
12.4 \isacommand{ML}\isamarkupfalse%
12.5 \ {\isachardoublequoteopen}Pretty{\isachardot}margin{\isacharunderscore}default\ {\isacharcolon}{\isacharequal}\ {\isadigit{6}}{\isadigit{4}}{\isachardoublequoteclose}\isanewline
12.6 \isacommand{ML}\isamarkupfalse%
12.7 -\ {\isachardoublequoteopen}ThyOutput{\isachardot}indent\ {\isacharcolon}{\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}%
12.8 +\ {\isachardoublequoteopen}Thy{\isacharunderscore}Output{\isachardot}indent\ {\isacharcolon}{\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}%
12.9 \endisatagML
12.10 {\isafoldML}%
12.11 %
13.1 --- a/doc-src/TutorialI/Types/document/Pairs.tex Mon May 31 19:36:13 2010 +0200
13.2 +++ b/doc-src/TutorialI/Types/document/Pairs.tex Mon May 31 21:06:57 2010 +0200
13.3 @@ -60,7 +60,7 @@
13.4 Internally, \isa{{\isasymlambda}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isachardot}\ t} becomes \isa{split\ {\isacharparenleft}{\isasymlambda}x\ y{\isachardot}\ t{\isacharparenright}}, where
13.5 \cdx{split} is the uncurrying function of type \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}c{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}c} defined as
13.6 \begin{center}
13.7 -\isa{split\ {\isasymequiv}\ {\isasymlambda}c\ p{\isachardot}\ c\ {\isacharparenleft}fst\ p{\isacharparenright}\ {\isacharparenleft}snd\ p{\isacharparenright}}
13.8 +\isa{split\ {\isacharequal}\ {\isacharparenleft}{\isasymlambda}c\ p{\isachardot}\ c\ {\isacharparenleft}fst\ p{\isacharparenright}\ {\isacharparenleft}snd\ p{\isacharparenright}{\isacharparenright}}
13.9 \hfill(\isa{split{\isacharunderscore}def})
13.10 \end{center}
13.11 Pattern matching in
14.1 --- a/doc-src/TutorialI/settings.ML Mon May 31 19:36:13 2010 +0200
14.2 +++ b/doc-src/TutorialI/settings.ML Mon May 31 21:06:57 2010 +0200
14.3 @@ -1,3 +1,3 @@
14.4 (* $Id$ *)
14.5
14.6 -ThyOutput.indent := 5;
14.7 +Thy_Output.indent := 5;
15.1 --- a/doc-src/antiquote_setup.ML Mon May 31 19:36:13 2010 +0200
15.2 +++ b/doc-src/antiquote_setup.ML Mon May 31 21:06:57 2010 +0200
15.3 @@ -35,7 +35,7 @@
15.4
15.5 val verbatim = space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|";
15.6
15.7 -val _ = ThyOutput.antiquotation "verbatim" (Scan.lift Args.name)
15.8 +val _ = Thy_Output.antiquotation "verbatim" (Scan.lift Args.name)
15.9 (K (split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"));
15.10
15.11
15.12 @@ -56,7 +56,7 @@
15.13
15.14 fun ml_functor (txt, _) = "ML_Env.check_functor " ^ ML_Syntax.print_string txt;
15.15
15.16 -fun index_ml name kind ml = ThyOutput.antiquotation name
15.17 +fun index_ml name kind ml = Thy_Output.antiquotation name
15.18 (Scan.lift (Args.name -- Scan.optional (Args.colon |-- Args.name) ""))
15.19 (fn {context = ctxt, ...} => fn (txt1, txt2) =>
15.20 let
15.21 @@ -71,8 +71,8 @@
15.22 in
15.23 "\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string txt1 ^ "}" ^
15.24 (txt'
15.25 - |> (if ! ThyOutput.quotes then quote else I)
15.26 - |> (if ! ThyOutput.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
15.27 + |> (if ! Thy_Output.quotes then quote else I)
15.28 + |> (if ! Thy_Output.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
15.29 else split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"))
15.30 end);
15.31
15.32 @@ -89,30 +89,30 @@
15.33
15.34 (* named theorems *)
15.35
15.36 -val _ = ThyOutput.antiquotation "named_thms"
15.37 +val _ = Thy_Output.antiquotation "named_thms"
15.38 (Scan.repeat (Attrib.thm -- Scan.lift (Args.parens Args.name)))
15.39 (fn {context = ctxt, ...} =>
15.40 - map (apfst (ThyOutput.pretty_thm ctxt))
15.41 - #> (if ! ThyOutput.quotes then map (apfst Pretty.quote) else I)
15.42 - #> (if ! ThyOutput.display
15.43 + map (apfst (Thy_Output.pretty_thm ctxt))
15.44 + #> (if ! Thy_Output.quotes then map (apfst Pretty.quote) else I)
15.45 + #> (if ! Thy_Output.display
15.46 then
15.47 map (fn (p, name) =>
15.48 - Output.output (Pretty.string_of (Pretty.indent (! ThyOutput.indent) p)) ^
15.49 - "\\rulename{" ^ Output.output (Pretty.str_of (ThyOutput.pretty_text name)) ^ "}")
15.50 + Output.output (Pretty.string_of (Pretty.indent (! Thy_Output.indent) p)) ^
15.51 + "\\rulename{" ^ Output.output (Pretty.str_of (Thy_Output.pretty_text name)) ^ "}")
15.52 #> space_implode "\\par\\smallskip%\n"
15.53 #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
15.54 else
15.55 map (fn (p, name) =>
15.56 Output.output (Pretty.str_of p) ^
15.57 - "\\rulename{" ^ Output.output (Pretty.str_of (ThyOutput.pretty_text name)) ^ "}")
15.58 + "\\rulename{" ^ Output.output (Pretty.str_of (Thy_Output.pretty_text name)) ^ "}")
15.59 #> space_implode "\\par\\smallskip%\n"
15.60 #> enclose "\\isa{" "}"));
15.61
15.62
15.63 (* theory file *)
15.64
15.65 -val _ = ThyOutput.antiquotation "thy_file" (Scan.lift Args.name)
15.66 - (fn _ => fn name => (ThyLoad.check_thy Path.current name; ThyOutput.output [Pretty.str name]));
15.67 +val _ = Thy_Output.antiquotation "thy_file" (Scan.lift Args.name)
15.68 + (fn _ => fn name => (Thy_Load.check_thy Path.current name; Thy_Output.output [Pretty.str name]));
15.69
15.70
15.71 (* Isabelle/Isar entities (with index) *)
15.72 @@ -131,7 +131,7 @@
15.73 val arg = enclose "{" "}" o clean_string;
15.74
15.75 fun entity check markup kind index =
15.76 - ThyOutput.antiquotation
15.77 + Thy_Output.antiquotation
15.78 (translate (fn " " => "_" | c => c) kind ^
15.79 (case index of NONE => "" | SOME true => "_def" | SOME false => "_ref"))
15.80 (Scan.lift (Scan.optional (Args.parens Args.name) "" -- Args.name))
15.81 @@ -152,8 +152,8 @@
15.82 idx ^
15.83 (Output.output name
15.84 |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}")
15.85 - |> (if ! ThyOutput.quotes then quote else I)
15.86 - |> (if ! ThyOutput.display then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
15.87 + |> (if ! Thy_Output.quotes then quote else I)
15.88 + |> (if ! Thy_Output.display then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
15.89 else hyper o enclose "\\mbox{\\isa{" "}}"))
15.90 else error ("Bad " ^ kind ^ " " ^ quote name)
15.91 end);
15.92 @@ -174,14 +174,14 @@
15.93 val _ = entity_antiqs no_check "" "fact";
15.94 val _ = entity_antiqs no_check "" "variable";
15.95 val _ = entity_antiqs no_check "" "case";
15.96 -val _ = entity_antiqs (K ThyOutput.defined_command) "" "antiquotation";
15.97 -val _ = entity_antiqs (K ThyOutput.defined_option) "" "antiquotation option";
15.98 +val _ = entity_antiqs (K Thy_Output.defined_command) "" "antiquotation";
15.99 +val _ = entity_antiqs (K Thy_Output.defined_option) "" "antiquotation option";
15.100 val _ = entity_antiqs (fn _ => fn name => is_some (OS.Process.getEnv name)) "isatt" "setting";
15.101 val _ = entity_antiqs no_check "" "inference";
15.102 val _ = entity_antiqs no_check "isatt" "executable";
15.103 val _ = entity_antiqs (K check_tool) "isatt" "tool";
15.104 val _ = entity_antiqs (K (File.exists o Path.explode)) "isatt" "file";
15.105 -val _ = entity_antiqs (K ThyInfo.known_thy) "" "theory";
15.106 +val _ = entity_antiqs (K Thy_Info.known_thy) "" "theory";
15.107
15.108 end;
15.109
16.1 --- a/doc-src/more_antiquote.ML Mon May 31 19:36:13 2010 +0200
16.2 +++ b/doc-src/more_antiquote.ML Mon May 31 21:06:57 2010 +0200
16.3 @@ -64,8 +64,8 @@
16.4
16.5 in
16.6
16.7 -val _ = ThyOutput.antiquotation "class" (Scan.lift Args.name) (pr_class o #context);
16.8 -val _ = ThyOutput.antiquotation "type" (Scan.lift Args.name) (pr_type o #context);
16.9 +val _ = Thy_Output.antiquotation "class" (Scan.lift Args.name) (pr_class o #context);
16.10 +val _ = Thy_Output.antiquotation "type" (Scan.lift Args.name) (pr_type o #context);
16.11
16.12 end;
16.13
16.14 @@ -95,11 +95,11 @@
16.15 |> snd
16.16 |> map_filter (fn (_, (some_thm, proper)) => if proper then some_thm else NONE)
16.17 |> map (holize o no_vars ctxt o AxClass.overload thy);
16.18 - in ThyOutput.output (ThyOutput.maybe_pretty_source (pretty_thm ctxt) src thms) end;
16.19 + in Thy_Output.output (Thy_Output.maybe_pretty_source (pretty_thm ctxt) src thms) end;
16.20
16.21 in
16.22
16.23 -val _ = ThyOutput.antiquotation "code_thms" Args.term
16.24 +val _ = Thy_Output.antiquotation "code_thms" Args.term
16.25 (fn {source, context, ...} => pretty_code_thm source context);
16.26
16.27 end;
16.28 @@ -123,7 +123,7 @@
16.29
16.30 in
16.31
16.32 -val _ = ThyOutput.antiquotation "code_stmts"
16.33 +val _ = Thy_Output.antiquotation "code_stmts"
16.34 (parse_const_terms -- Scan.repeat parse_names -- Scan.lift (Args.parens Args.name))
16.35 (fn {context = ctxt, ...} => fn ((mk_cs, mk_stmtss), target) =>
16.36 let val thy = ProofContext.theory_of ctxt in
17.1 --- a/doc-src/rail.ML Mon May 31 19:36:13 2010 +0200
17.2 +++ b/doc-src/rail.ML Mon May 31 21:06:57 2010 +0200
17.3 @@ -67,14 +67,14 @@
17.4 ("fact", ("", no_check, true)),
17.5 ("variable", ("", no_check, true)),
17.6 ("case", ("", no_check, true)),
17.7 - ("antiquotation", ("", K ThyOutput.defined_command, true)),
17.8 - ("antiquotation option", ("", K ThyOutput.defined_option, true)), (* kann mein scanner nicht erkennen *)
17.9 + ("antiquotation", ("", K Thy_Output.defined_command, true)),
17.10 + ("antiquotation option", ("", K Thy_Output.defined_option, true)), (* kann mein scanner nicht erkennen *)
17.11 ("setting", ("isatt", (fn _ => fn name => is_some (OS.Process.getEnv name)), true)),
17.12 ("inference", ("", no_check, true)),
17.13 ("executable", ("isatt", no_check, true)),
17.14 ("tool", ("isatt", K check_tool, true)),
17.15 ("file", ("isatt", K (File.exists o Path.explode), true)),
17.16 - ("theory", ("", K ThyInfo.known_thy, true))
17.17 + ("theory", ("", K Thy_Info.known_thy, true))
17.18 ];
17.19
17.20 in
17.21 @@ -97,8 +97,8 @@
17.22 (idx ^
17.23 (Output.output name
17.24 |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}")
17.25 - |> (if ! ThyOutput.quotes then quote else I)
17.26 - |> (if ! ThyOutput.display then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
17.27 + |> (if ! Thy_Output.quotes then quote else I)
17.28 + |> (if ! Thy_Output.display then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
17.29 else hyper o enclose "\\mbox{\\isa{" "}}")), style)
17.30 else ("Bad " ^ kind ^ " " ^ name, false)
17.31 end;
17.32 @@ -473,7 +473,7 @@
17.33 |> parse
17.34 |> print;
17.35
17.36 -val _ = ThyOutput.antiquotation "rail" (Scan.lift (Parse.position Args.name))
17.37 +val _ = Thy_Output.antiquotation "rail" (Scan.lift (Parse.position Args.name))
17.38 (fn {context = ctxt,...} => fn txt => process txt ctxt);
17.39
17.40 end;
18.1 --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Mon May 31 19:36:13 2010 +0200
18.2 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Mon May 31 21:06:57 2010 +0200
18.3 @@ -219,7 +219,7 @@
18.4 then NONE
18.5 else
18.6 let
18.7 - val _ = List.app (SimpleThread.interrupt o #1) cancelling;
18.8 + val _ = List.app (Simple_Thread.interrupt o #1) cancelling;
18.9 val cancelling' = filter (Thread.isActive o #1) cancelling;
18.10 val state' = make_state manager timeout_heap' active cancelling' messages store;
18.11 in SOME (map #2 timeout_threads, state') end
19.1 --- a/src/HOL/Tools/Datatype/datatype_data.ML Mon May 31 19:36:13 2010 +0200
19.2 +++ b/src/HOL/Tools/Datatype/datatype_data.ML Mon May 31 21:06:57 2010 +0200
19.3 @@ -236,7 +236,7 @@
19.4
19.5 (** document antiquotation **)
19.6
19.7 -val _ = ThyOutput.antiquotation "datatype" (Args.type_name true)
19.8 +val _ = Thy_Output.antiquotation "datatype" (Args.type_name true)
19.9 (fn {source = src, context = ctxt, ...} => fn dtco =>
19.10 let
19.11 val thy = ProofContext.theory_of ctxt;
19.12 @@ -257,7 +257,7 @@
19.13 Pretty.str " =" :: Pretty.brk 1 ::
19.14 flat (separate [Pretty.brk 1, Pretty.str "| "]
19.15 (map (single o pretty_constr) cos)));
19.16 - in ThyOutput.output (ThyOutput.maybe_pretty_source (K pretty_datatype) src [()]) end);
19.17 + in Thy_Output.output (Thy_Output.maybe_pretty_source (K pretty_datatype) src [()]) end);
19.18
19.19
19.20
20.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML Mon May 31 19:36:13 2010 +0200
20.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Mon May 31 21:06:57 2010 +0200
20.3 @@ -181,7 +181,7 @@
20.4 val ctxt = Proof.context_of state
20.5 (* FIXME: reintroduce code before new release:
20.6
20.7 - val nitpick_thy = ThyInfo.get_theory "Nitpick"
20.8 + val nitpick_thy = Thy_Info.get_theory "Nitpick"
20.9 val _ = Theory.subthy (nitpick_thy, thy) orelse
20.10 error "You must import the theory \"Nitpick\" to use Nitpick"
20.11 *)
21.1 --- a/src/Pure/Concurrent/future.ML Mon May 31 19:36:13 2010 +0200
21.2 +++ b/src/Pure/Concurrent/future.ML Mon May 31 21:06:57 2010 +0200
21.3 @@ -126,7 +126,7 @@
21.4 val lock = Mutex.mutex ();
21.5 in
21.6
21.7 -fun SYNCHRONIZED name = SimpleThread.synchronized name lock;
21.8 +fun SYNCHRONIZED name = Simple_Thread.synchronized name lock;
21.9
21.10 fun wait cond = (*requires SYNCHRONIZED*)
21.11 Multithreading.sync_wait NONE NONE cond lock;
21.12 @@ -238,7 +238,7 @@
21.13 | SOME work => (execute work; worker_loop name));
21.14
21.15 fun worker_start name = (*requires SYNCHRONIZED*)
21.16 - Unsynchronized.change workers (cons (SimpleThread.fork false (fn () => worker_loop name),
21.17 + Unsynchronized.change workers (cons (Simple_Thread.fork false (fn () => worker_loop name),
21.18 Unsynchronized.ref Working));
21.19
21.20
21.21 @@ -371,7 +371,7 @@
21.22 fun scheduler_check () = (*requires SYNCHRONIZED*)
21.23 (do_shutdown := false;
21.24 if scheduler_active () then ()
21.25 - else scheduler := SOME (SimpleThread.fork false scheduler_loop));
21.26 + else scheduler := SOME (Simple_Thread.fork false scheduler_loop));
21.27
21.28
21.29
22.1 --- a/src/Pure/Concurrent/simple_thread.ML Mon May 31 19:36:13 2010 +0200
22.2 +++ b/src/Pure/Concurrent/simple_thread.ML Mon May 31 21:06:57 2010 +0200
22.3 @@ -12,7 +12,7 @@
22.4 val synchronized: string -> Mutex.mutex -> (unit -> 'a) -> 'a
22.5 end;
22.6
22.7 -structure SimpleThread: SIMPLE_THREAD =
22.8 +structure Simple_Thread: SIMPLE_THREAD =
22.9 struct
22.10
22.11 fun attributes interrupts =
23.1 --- a/src/Pure/Concurrent/single_assignment.ML Mon May 31 19:36:13 2010 +0200
23.2 +++ b/src/Pure/Concurrent/single_assignment.ML Mon May 31 21:06:57 2010 +0200
23.3 @@ -32,7 +32,7 @@
23.4 fun peek (Var {var, ...}) = SingleAssignment.savalue var;
23.5
23.6 fun await (v as Var {name, lock, cond, var}) =
23.7 - SimpleThread.synchronized name lock (fn () =>
23.8 + Simple_Thread.synchronized name lock (fn () =>
23.9 let
23.10 fun wait () =
23.11 (case peek v of
23.12 @@ -44,7 +44,7 @@
23.13 in wait () end);
23.14
23.15 fun assign (v as Var {name, lock, cond, var}) x =
23.16 - SimpleThread.synchronized name lock (fn () =>
23.17 + Simple_Thread.synchronized name lock (fn () =>
23.18 (case peek v of
23.19 SOME _ => raise Fail ("Duplicate assignment to variable " ^ quote name)
23.20 | NONE =>
24.1 --- a/src/Pure/Concurrent/synchronized.ML Mon May 31 19:36:13 2010 +0200
24.2 +++ b/src/Pure/Concurrent/synchronized.ML Mon May 31 21:06:57 2010 +0200
24.3 @@ -39,7 +39,7 @@
24.4 (* synchronized access *)
24.5
24.6 fun timed_access (Var {name, lock, cond, var}) time_limit f =
24.7 - SimpleThread.synchronized name lock (fn () =>
24.8 + Simple_Thread.synchronized name lock (fn () =>
24.9 let
24.10 fun try_change () =
24.11 let val x = ! var in
25.1 --- a/src/Pure/Concurrent/task_queue.ML Mon May 31 19:36:13 2010 +0200
25.2 +++ b/src/Pure/Concurrent/task_queue.ML Mon May 31 21:06:57 2010 +0200
25.3 @@ -162,7 +162,7 @@
25.4 val tasks = Inttab.lookup_list groups (group_id group);
25.5 val running =
25.6 fold (get_job jobs #> (fn Running t => insert Thread.equal t | _ => I)) tasks [];
25.7 - val _ = List.app SimpleThread.interrupt running;
25.8 + val _ = List.app Simple_Thread.interrupt running;
25.9 in null running end;
25.10
25.11 fun cancel_all (Queue {groups, jobs}) =
25.12 @@ -173,7 +173,7 @@
25.13 Running t => (insert eq_group group groups, insert Thread.equal t running)
25.14 | _ => (groups, running)));
25.15 val (running_groups, running) = Task_Graph.fold (cancel_job o #1 o #2) jobs ([], []);
25.16 - val _ = List.app SimpleThread.interrupt running;
25.17 + val _ = List.app Simple_Thread.interrupt running;
25.18 in running_groups end;
25.19
25.20
26.1 --- a/src/Pure/General/scan.ML Mon May 31 19:36:13 2010 +0200
26.2 +++ b/src/Pure/General/scan.ML Mon May 31 21:06:57 2010 +0200
26.3 @@ -322,5 +322,5 @@
26.4
26.5 end;
26.6
26.7 -structure BasicScan: BASIC_SCAN = Scan;
26.8 -open BasicScan;
26.9 +structure Basic_Scan: BASIC_SCAN = Scan;
26.10 +open Basic_Scan;
27.1 --- a/src/Pure/Isar/isar_cmd.ML Mon May 31 19:36:13 2010 +0200
27.2 +++ b/src/Pure/Isar/isar_cmd.ML Mon May 31 21:06:57 2010 +0200
27.3 @@ -85,7 +85,7 @@
27.4 val proof_markup: Symbol_Pos.text * Position.T -> Toplevel.transition -> Toplevel.transition
27.5 end;
27.6
27.7 -structure IsarCmd: ISAR_CMD =
27.8 +structure Isar_Cmd: ISAR_CMD =
27.9 struct
27.10
27.11
27.12 @@ -272,10 +272,10 @@
27.13 (* init and exit *)
27.14
27.15 fun init_theory (name, imports, uses) =
27.16 - Toplevel.init_theory name (ThyInfo.begin_theory name imports (map (apfst Path.explode) uses))
27.17 + Toplevel.init_theory name (Thy_Info.begin_theory name imports (map (apfst Path.explode) uses))
27.18 (fn thy =>
27.19 - if ThyInfo.check_known_thy (Context.theory_name thy)
27.20 - then ThyInfo.end_theory thy else ());
27.21 + if Thy_Info.check_known_thy (Context.theory_name thy)
27.22 + then Thy_Info.end_theory thy else ());
27.23
27.24 val exit = Toplevel.keep (fn state =>
27.25 (Context.set_thread_data (try Toplevel.generic_theory_of state);
27.26 @@ -384,18 +384,18 @@
27.27 val print_methods = Toplevel.unknown_theory o
27.28 Toplevel.keep (Method.print_methods o Toplevel.theory_of);
27.29
27.30 -val print_antiquotations = Toplevel.imperative ThyOutput.print_antiquotations;
27.31 +val print_antiquotations = Toplevel.imperative Thy_Output.print_antiquotations;
27.32
27.33 val thy_deps = Toplevel.unknown_theory o Toplevel.keep (fn state =>
27.34 let
27.35 val thy = Toplevel.theory_of state;
27.36 - val all_thys = sort ThyInfo.thy_ord (thy :: Theory.ancestors_of thy);
27.37 + val all_thys = sort Thy_Info.thy_ord (thy :: Theory.ancestors_of thy);
27.38 val gr = all_thys |> map (fn node =>
27.39 let
27.40 val name = Context.theory_name node;
27.41 val parents = map Context.theory_name (Theory.parents_of node);
27.42 val dir = Present.session_name node;
27.43 - val unfold = not (ThyInfo.known_thy name andalso ThyInfo.is_finished name);
27.44 + val unfold = not (Thy_Info.known_thy name andalso Thy_Info.is_finished name);
27.45 in {name = name, ID = name, parents = parents, dir = dir, unfold = unfold, path = ""} end);
27.46 in Present.display_graph gr end);
27.47
27.48 @@ -427,8 +427,8 @@
27.49 Thm_Deps.unused_thms
27.50 (case opt_range of
27.51 NONE => (Theory.parents_of thy, [thy])
27.52 - | SOME (xs, NONE) => (map ThyInfo.get_theory xs, [thy])
27.53 - | SOME (xs, SOME ys) => (map ThyInfo.get_theory xs, map ThyInfo.get_theory ys))
27.54 + | SOME (xs, NONE) => (map Thy_Info.get_theory xs, [thy])
27.55 + | SOME (xs, SOME ys) => (map Thy_Info.get_theory xs, map Thy_Info.get_theory ys))
27.56 |> map pretty_thm |> Pretty.chunks |> Pretty.writeln
27.57 end);
27.58
27.59 @@ -517,7 +517,7 @@
27.60
27.61 fun check_text (txt, pos) state =
27.62 (Position.report Markup.doc_source pos;
27.63 - ignore (ThyOutput.eval_antiquote (#1 (Keyword.get_lexicons ())) state (txt, pos)));
27.64 + ignore (Thy_Output.eval_antiquote (#1 (Keyword.get_lexicons ())) state (txt, pos)));
27.65
27.66 fun header_markup txt = Toplevel.keep (fn state =>
27.67 if Toplevel.is_toplevel state then check_text txt state
28.1 --- a/src/Pure/Isar/isar_document.ML Mon May 31 19:36:13 2010 +0200
28.2 +++ b/src/Pure/Isar/isar_document.ML Mon May 31 21:06:57 2010 +0200
28.3 @@ -181,7 +181,7 @@
28.4
28.5 fun begin_document (id: document_id) path =
28.6 let
28.7 - val (dir, name) = ThyLoad.split_thy_path path;
28.8 + val (dir, name) = Thy_Load.split_thy_path path;
28.9 val _ = define_document id (make_document dir name no_entries);
28.10 in () end;
28.11
28.12 @@ -197,8 +197,8 @@
28.13 (case Lazy.force end_state of
28.14 SOME st =>
28.15 (Toplevel.run_command name (Toplevel.put_id id (Toplevel.commit_exit Position.none)) st;
28.16 - ThyInfo.touch_child_thys name;
28.17 - ThyInfo.register_thy name)
28.18 + Thy_Info.touch_child_thys name;
28.19 + Thy_Info.register_thy name)
28.20 | NONE => error ("Failed to finish theory " ^ quote name)));
28.21 in () end);
28.22
29.1 --- a/src/Pure/Isar/isar_syn.ML Mon May 31 19:36:13 2010 +0200
29.2 +++ b/src/Pure/Isar/isar_syn.ML Mon May 31 21:06:57 2010 +0200
29.3 @@ -4,7 +4,7 @@
29.4 Isar/Pure outer syntax.
29.5 *)
29.6
29.7 -structure IsarSyn: sig end =
29.8 +structure Isar_Syn: sig end =
29.9 struct
29.10
29.11 (** keywords **)
29.12 @@ -28,7 +28,7 @@
29.13
29.14 val _ =
29.15 Outer_Syntax.command "theory" "begin theory" (Keyword.tag_theory Keyword.thy_begin)
29.16 - (Thy_Header.args >> (Toplevel.print oo IsarCmd.init_theory));
29.17 + (Thy_Header.args >> (Toplevel.print oo Isar_Cmd.init_theory));
29.18
29.19 val _ =
29.20 Outer_Syntax.command "end" "end (local) theory" (Keyword.tag_theory Keyword.thy_end)
29.21 @@ -38,43 +38,43 @@
29.22
29.23 (** markup commands **)
29.24
29.25 -val _ = Outer_Syntax.markup_command ThyOutput.Markup "header" "theory header" Keyword.diag
29.26 - (Parse.doc_source >> IsarCmd.header_markup);
29.27 +val _ = Outer_Syntax.markup_command Thy_Output.Markup "header" "theory header" Keyword.diag
29.28 + (Parse.doc_source >> Isar_Cmd.header_markup);
29.29
29.30 -val _ = Outer_Syntax.markup_command ThyOutput.Markup "chapter" "chapter heading"
29.31 - Keyword.thy_heading (Parse.opt_target -- Parse.doc_source >> IsarCmd.local_theory_markup);
29.32 +val _ = Outer_Syntax.markup_command Thy_Output.Markup "chapter" "chapter heading"
29.33 + Keyword.thy_heading (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
29.34
29.35 -val _ = Outer_Syntax.markup_command ThyOutput.Markup "section" "section heading"
29.36 - Keyword.thy_heading (Parse.opt_target -- Parse.doc_source >> IsarCmd.local_theory_markup);
29.37 +val _ = Outer_Syntax.markup_command Thy_Output.Markup "section" "section heading"
29.38 + Keyword.thy_heading (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
29.39
29.40 -val _ = Outer_Syntax.markup_command ThyOutput.Markup "subsection" "subsection heading"
29.41 - Keyword.thy_heading (Parse.opt_target -- Parse.doc_source >> IsarCmd.local_theory_markup);
29.42 +val _ = Outer_Syntax.markup_command Thy_Output.Markup "subsection" "subsection heading"
29.43 + Keyword.thy_heading (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
29.44
29.45 val _ =
29.46 - Outer_Syntax.markup_command ThyOutput.Markup "subsubsection" "subsubsection heading"
29.47 - Keyword.thy_heading (Parse.opt_target -- Parse.doc_source >> IsarCmd.local_theory_markup);
29.48 + Outer_Syntax.markup_command Thy_Output.Markup "subsubsection" "subsubsection heading"
29.49 + Keyword.thy_heading (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
29.50
29.51 -val _ = Outer_Syntax.markup_command ThyOutput.MarkupEnv "text" "formal comment (theory)"
29.52 - Keyword.thy_decl (Parse.opt_target -- Parse.doc_source >> IsarCmd.local_theory_markup);
29.53 +val _ = Outer_Syntax.markup_command Thy_Output.MarkupEnv "text" "formal comment (theory)"
29.54 + Keyword.thy_decl (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
29.55
29.56 -val _ = Outer_Syntax.markup_command ThyOutput.Verbatim "text_raw" "raw document preparation text"
29.57 - Keyword.thy_decl (Parse.opt_target -- Parse.doc_source >> IsarCmd.local_theory_markup);
29.58 +val _ = Outer_Syntax.markup_command Thy_Output.Verbatim "text_raw" "raw document preparation text"
29.59 + Keyword.thy_decl (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
29.60
29.61 -val _ = Outer_Syntax.markup_command ThyOutput.Markup "sect" "formal comment (proof)"
29.62 - (Keyword.tag_proof Keyword.prf_heading) (Parse.doc_source >> IsarCmd.proof_markup);
29.63 +val _ = Outer_Syntax.markup_command Thy_Output.Markup "sect" "formal comment (proof)"
29.64 + (Keyword.tag_proof Keyword.prf_heading) (Parse.doc_source >> Isar_Cmd.proof_markup);
29.65
29.66 -val _ = Outer_Syntax.markup_command ThyOutput.Markup "subsect" "formal comment (proof)"
29.67 - (Keyword.tag_proof Keyword.prf_heading) (Parse.doc_source >> IsarCmd.proof_markup);
29.68 +val _ = Outer_Syntax.markup_command Thy_Output.Markup "subsect" "formal comment (proof)"
29.69 + (Keyword.tag_proof Keyword.prf_heading) (Parse.doc_source >> Isar_Cmd.proof_markup);
29.70
29.71 -val _ = Outer_Syntax.markup_command ThyOutput.Markup "subsubsect" "formal comment (proof)"
29.72 - (Keyword.tag_proof Keyword.prf_heading) (Parse.doc_source >> IsarCmd.proof_markup);
29.73 +val _ = Outer_Syntax.markup_command Thy_Output.Markup "subsubsect" "formal comment (proof)"
29.74 + (Keyword.tag_proof Keyword.prf_heading) (Parse.doc_source >> Isar_Cmd.proof_markup);
29.75
29.76 -val _ = Outer_Syntax.markup_command ThyOutput.MarkupEnv "txt" "formal comment (proof)"
29.77 - (Keyword.tag_proof Keyword.prf_decl) (Parse.doc_source >> IsarCmd.proof_markup);
29.78 +val _ = Outer_Syntax.markup_command Thy_Output.MarkupEnv "txt" "formal comment (proof)"
29.79 + (Keyword.tag_proof Keyword.prf_decl) (Parse.doc_source >> Isar_Cmd.proof_markup);
29.80
29.81 -val _ = Outer_Syntax.markup_command ThyOutput.Verbatim "txt_raw"
29.82 +val _ = Outer_Syntax.markup_command Thy_Output.Verbatim "txt_raw"
29.83 "raw document preparation text (proof)" (Keyword.tag_proof Keyword.prf_decl)
29.84 - (Parse.doc_source >> IsarCmd.proof_markup);
29.85 + (Parse.doc_source >> Isar_Cmd.proof_markup);
29.86
29.87
29.88
29.89 @@ -185,7 +185,7 @@
29.90 Outer_Syntax.command "axioms" "state arbitrary propositions (axiomatic!)" Keyword.thy_decl
29.91 (Scan.repeat1 Parse_Spec.spec >>
29.92 (Toplevel.theory o
29.93 - (IsarCmd.add_axioms o
29.94 + (Isar_Cmd.add_axioms o
29.95 tap (fn _ => legacy_feature "Old 'axioms' command -- use 'axiomatization' instead"))));
29.96
29.97 val opt_unchecked_overloaded =
29.98 @@ -197,7 +197,7 @@
29.99 Outer_Syntax.command "defs" "define constants" Keyword.thy_decl
29.100 (opt_unchecked_overloaded --
29.101 Scan.repeat1 (Parse_Spec.thm_name ":" -- Parse.prop >> (fn ((x, y), z) => ((x, z), y)))
29.102 - >> (Toplevel.theory o IsarCmd.add_defs));
29.103 + >> (Toplevel.theory o Isar_Cmd.add_defs));
29.104
29.105
29.106 (* old constdefs *)
29.107 @@ -296,10 +296,10 @@
29.108 ((Parse.opt_keyword "open" >> not) -- Scan.repeat1 Parse.xname >>
29.109 (Toplevel.theory o uncurry hide));
29.110
29.111 -val _ = hide_names "hide_class" IsarCmd.hide_class "classes";
29.112 -val _ = hide_names "hide_type" IsarCmd.hide_type "types";
29.113 -val _ = hide_names "hide_const" IsarCmd.hide_const "constants";
29.114 -val _ = hide_names "hide_fact" IsarCmd.hide_fact "facts";
29.115 +val _ = hide_names "hide_class" Isar_Cmd.hide_class "classes";
29.116 +val _ = hide_names "hide_type" Isar_Cmd.hide_type "types";
29.117 +val _ = hide_names "hide_const" Isar_Cmd.hide_const "constants";
29.118 +val _ = hide_names "hide_fact" Isar_Cmd.hide_fact "facts";
29.119
29.120
29.121 (* use ML text *)
29.122 @@ -314,7 +314,7 @@
29.123 val _ =
29.124 Outer_Syntax.command "use" "ML text from file" (Keyword.tag_ml Keyword.thy_decl)
29.125 (Parse.path >>
29.126 - (fn path => Toplevel.generic_theory (ThyInfo.exec_file false path #> propagate_env)));
29.127 + (fn path => Toplevel.generic_theory (Thy_Info.exec_file false path #> propagate_env)));
29.128
29.129 val _ =
29.130 Outer_Syntax.command "ML" "ML text within theory or local theory"
29.131 @@ -331,19 +331,19 @@
29.132
29.133 val _ =
29.134 Outer_Syntax.command "ML_val" "diagnostic ML text" (Keyword.tag_ml Keyword.diag)
29.135 - (Parse.ML_source >> IsarCmd.ml_diag true);
29.136 + (Parse.ML_source >> Isar_Cmd.ml_diag true);
29.137
29.138 val _ =
29.139 Outer_Syntax.command "ML_command" "diagnostic ML text (silent)" (Keyword.tag_ml Keyword.diag)
29.140 - (Parse.ML_source >> (Toplevel.no_timing oo IsarCmd.ml_diag false));
29.141 + (Parse.ML_source >> (Toplevel.no_timing oo Isar_Cmd.ml_diag false));
29.142
29.143 val _ =
29.144 Outer_Syntax.command "setup" "ML theory setup" (Keyword.tag_ml Keyword.thy_decl)
29.145 - (Parse.ML_source >> (Toplevel.theory o IsarCmd.global_setup));
29.146 + (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.global_setup));
29.147
29.148 val _ =
29.149 Outer_Syntax.local_theory "local_setup" "ML local theory setup" (Keyword.tag_ml Keyword.thy_decl)
29.150 - (Parse.ML_source >> IsarCmd.local_setup);
29.151 + (Parse.ML_source >> Isar_Cmd.local_setup);
29.152
29.153 val _ =
29.154 Outer_Syntax.command "attribute_setup" "define attribute in ML" (Keyword.tag_ml Keyword.thy_decl)
29.155 @@ -357,14 +357,14 @@
29.156
29.157 val _ =
29.158 Outer_Syntax.local_theory "declaration" "generic ML declaration" (Keyword.tag_ml Keyword.thy_decl)
29.159 - (Parse.opt_keyword "pervasive" -- Parse.ML_source >> uncurry IsarCmd.declaration);
29.160 + (Parse.opt_keyword "pervasive" -- Parse.ML_source >> uncurry Isar_Cmd.declaration);
29.161
29.162 val _ =
29.163 Outer_Syntax.local_theory "simproc_setup" "define simproc in ML" (Keyword.tag_ml Keyword.thy_decl)
29.164 (Parse.name --
29.165 (Parse.$$$ "(" |-- Parse.enum1 "|" Parse.term --| Parse.$$$ ")" --| Parse.$$$ "=") --
29.166 Parse.ML_source -- Scan.optional (Parse.$$$ "identifier" |-- Scan.repeat1 Parse.xname) []
29.167 - >> (fn (((a, b), c), d) => IsarCmd.simproc_setup a b c d));
29.168 + >> (fn (((a, b), c), d) => Isar_Cmd.simproc_setup a b c d));
29.169
29.170
29.171 (* translation functions *)
29.172 @@ -374,27 +374,27 @@
29.173 val _ =
29.174 Outer_Syntax.command "parse_ast_translation" "install parse ast translation functions"
29.175 (Keyword.tag_ml Keyword.thy_decl)
29.176 - (trfun >> (Toplevel.theory o IsarCmd.parse_ast_translation));
29.177 + (trfun >> (Toplevel.theory o Isar_Cmd.parse_ast_translation));
29.178
29.179 val _ =
29.180 Outer_Syntax.command "parse_translation" "install parse translation functions"
29.181 (Keyword.tag_ml Keyword.thy_decl)
29.182 - (trfun >> (Toplevel.theory o IsarCmd.parse_translation));
29.183 + (trfun >> (Toplevel.theory o Isar_Cmd.parse_translation));
29.184
29.185 val _ =
29.186 Outer_Syntax.command "print_translation" "install print translation functions"
29.187 (Keyword.tag_ml Keyword.thy_decl)
29.188 - (trfun >> (Toplevel.theory o IsarCmd.print_translation));
29.189 + (trfun >> (Toplevel.theory o Isar_Cmd.print_translation));
29.190
29.191 val _ =
29.192 Outer_Syntax.command "typed_print_translation" "install typed print translation functions"
29.193 (Keyword.tag_ml Keyword.thy_decl)
29.194 - (trfun >> (Toplevel.theory o IsarCmd.typed_print_translation));
29.195 + (trfun >> (Toplevel.theory o Isar_Cmd.typed_print_translation));
29.196
29.197 val _ =
29.198 Outer_Syntax.command "print_ast_translation" "install print ast translation functions"
29.199 (Keyword.tag_ml Keyword.thy_decl)
29.200 - (trfun >> (Toplevel.theory o IsarCmd.print_ast_translation));
29.201 + (trfun >> (Toplevel.theory o Isar_Cmd.print_ast_translation));
29.202
29.203
29.204 (* oracles *)
29.205 @@ -402,7 +402,7 @@
29.206 val _ =
29.207 Outer_Syntax.command "oracle" "declare oracle" (Keyword.tag_ml Keyword.thy_decl)
29.208 (Parse.position Parse.name -- (Parse.$$$ "=" |-- Parse.ML_source) >>
29.209 - (fn (x, y) => Toplevel.theory (IsarCmd.oracle x y)));
29.210 + (fn (x, y) => Toplevel.theory (Isar_Cmd.oracle x y)));
29.211
29.212
29.213 (* local theories *)
29.214 @@ -537,22 +537,22 @@
29.215 val _ =
29.216 Outer_Syntax.command "have" "state local goal"
29.217 (Keyword.tag_proof Keyword.prf_goal)
29.218 - (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.have));
29.219 + (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.have));
29.220
29.221 val _ =
29.222 Outer_Syntax.command "hence" "abbreviates \"then have\""
29.223 (Keyword.tag_proof Keyword.prf_goal)
29.224 - (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.hence));
29.225 + (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.hence));
29.226
29.227 val _ =
29.228 Outer_Syntax.command "show" "state local goal, solving current obligation"
29.229 (Keyword.tag_proof Keyword.prf_asm_goal)
29.230 - (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.show));
29.231 + (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.show));
29.232
29.233 val _ =
29.234 Outer_Syntax.command "thus" "abbreviates \"then show\""
29.235 (Keyword.tag_proof Keyword.prf_asm_goal)
29.236 - (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.thus));
29.237 + (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.thus));
29.238
29.239
29.240 (* facts *)
29.241 @@ -673,32 +673,32 @@
29.242 val _ =
29.243 Outer_Syntax.command "qed" "conclude (sub-)proof"
29.244 (Keyword.tag_proof Keyword.qed_block)
29.245 - (Scan.option Method.parse >> IsarCmd.qed);
29.246 + (Scan.option Method.parse >> Isar_Cmd.qed);
29.247
29.248 val _ =
29.249 Outer_Syntax.command "by" "terminal backward proof"
29.250 (Keyword.tag_proof Keyword.qed)
29.251 - (Method.parse -- Scan.option Method.parse >> IsarCmd.terminal_proof);
29.252 + (Method.parse -- Scan.option Method.parse >> Isar_Cmd.terminal_proof);
29.253
29.254 val _ =
29.255 Outer_Syntax.command ".." "default proof"
29.256 (Keyword.tag_proof Keyword.qed)
29.257 - (Scan.succeed IsarCmd.default_proof);
29.258 + (Scan.succeed Isar_Cmd.default_proof);
29.259
29.260 val _ =
29.261 Outer_Syntax.command "." "immediate proof"
29.262 (Keyword.tag_proof Keyword.qed)
29.263 - (Scan.succeed IsarCmd.immediate_proof);
29.264 + (Scan.succeed Isar_Cmd.immediate_proof);
29.265
29.266 val _ =
29.267 Outer_Syntax.command "done" "done proof"
29.268 (Keyword.tag_proof Keyword.qed)
29.269 - (Scan.succeed IsarCmd.done_proof);
29.270 + (Scan.succeed Isar_Cmd.done_proof);
29.271
29.272 val _ =
29.273 Outer_Syntax.command "sorry" "skip proof (quick-and-dirty mode only!)"
29.274 (Keyword.tag_proof Keyword.qed)
29.275 - (Scan.succeed IsarCmd.skip_proof);
29.276 + (Scan.succeed Isar_Cmd.skip_proof);
29.277
29.278 val _ =
29.279 Outer_Syntax.command "oops" "forget proof"
29.280 @@ -796,7 +796,7 @@
29.281
29.282 val _ =
29.283 Outer_Syntax.improper_command "pretty_setmargin" "change default margin for pretty printing"
29.284 - Keyword.diag (Parse.nat >> (Toplevel.no_timing oo IsarCmd.pretty_setmargin));
29.285 + Keyword.diag (Parse.nat >> (Toplevel.no_timing oo Isar_Cmd.pretty_setmargin));
29.286
29.287 val _ =
29.288 Outer_Syntax.improper_command "help" "print outer syntax commands" Keyword.diag
29.289 @@ -808,32 +808,32 @@
29.290
29.291 val _ =
29.292 Outer_Syntax.improper_command "print_configs" "print configuration options" Keyword.diag
29.293 - (Scan.succeed (Toplevel.no_timing o IsarCmd.print_configs));
29.294 + (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_configs));
29.295
29.296 val _ =
29.297 Outer_Syntax.improper_command "print_context" "print theory context name" Keyword.diag
29.298 - (Scan.succeed (Toplevel.no_timing o IsarCmd.print_context));
29.299 + (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_context));
29.300
29.301 val _ =
29.302 Outer_Syntax.improper_command "print_theory" "print logical theory contents (verbose!)"
29.303 - Keyword.diag (opt_bang >> (Toplevel.no_timing oo IsarCmd.print_theory));
29.304 + Keyword.diag (opt_bang >> (Toplevel.no_timing oo Isar_Cmd.print_theory));
29.305
29.306 val _ =
29.307 Outer_Syntax.improper_command "print_syntax" "print inner syntax of context (verbose!)"
29.308 - Keyword.diag (Scan.succeed (Toplevel.no_timing o IsarCmd.print_syntax));
29.309 + Keyword.diag (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_syntax));
29.310
29.311 val _ =
29.312 Outer_Syntax.improper_command "print_abbrevs" "print constant abbreviation of context"
29.313 - Keyword.diag (Scan.succeed (Toplevel.no_timing o IsarCmd.print_abbrevs));
29.314 + Keyword.diag (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_abbrevs));
29.315
29.316 val _ =
29.317 Outer_Syntax.improper_command "print_theorems"
29.318 "print theorems of local theory or proof context" Keyword.diag
29.319 - (opt_bang >> (Toplevel.no_timing oo IsarCmd.print_theorems));
29.320 + (opt_bang >> (Toplevel.no_timing oo Isar_Cmd.print_theorems));
29.321
29.322 val _ =
29.323 Outer_Syntax.improper_command "print_locales" "print locales of this theory" Keyword.diag
29.324 - (Scan.succeed (Toplevel.no_timing o IsarCmd.print_locales));
29.325 + (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_locales));
29.326
29.327 val _ =
29.328 Outer_Syntax.improper_command "print_classes" "print classes of this theory" Keyword.diag
29.329 @@ -842,89 +842,89 @@
29.330
29.331 val _ =
29.332 Outer_Syntax.improper_command "print_locale" "print locale of this theory" Keyword.diag
29.333 - (opt_bang -- Parse.xname >> (Toplevel.no_timing oo IsarCmd.print_locale));
29.334 + (opt_bang -- Parse.xname >> (Toplevel.no_timing oo Isar_Cmd.print_locale));
29.335
29.336 val _ =
29.337 Outer_Syntax.improper_command "print_interps"
29.338 "print interpretations of locale for this theory" Keyword.diag
29.339 - (Parse.xname >> (Toplevel.no_timing oo IsarCmd.print_registrations));
29.340 + (Parse.xname >> (Toplevel.no_timing oo Isar_Cmd.print_registrations));
29.341
29.342 val _ =
29.343 Outer_Syntax.improper_command "print_attributes" "print attributes of this theory" Keyword.diag
29.344 - (Scan.succeed (Toplevel.no_timing o IsarCmd.print_attributes));
29.345 + (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_attributes));
29.346
29.347 val _ =
29.348 Outer_Syntax.improper_command "print_simpset" "print context of Simplifier" Keyword.diag
29.349 - (Scan.succeed (Toplevel.no_timing o IsarCmd.print_simpset));
29.350 + (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_simpset));
29.351
29.352 val _ =
29.353 Outer_Syntax.improper_command "print_rules" "print intro/elim rules" Keyword.diag
29.354 - (Scan.succeed (Toplevel.no_timing o IsarCmd.print_rules));
29.355 + (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_rules));
29.356
29.357 val _ =
29.358 Outer_Syntax.improper_command "print_trans_rules" "print transitivity rules" Keyword.diag
29.359 - (Scan.succeed (Toplevel.no_timing o IsarCmd.print_trans_rules));
29.360 + (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_trans_rules));
29.361
29.362 val _ =
29.363 Outer_Syntax.improper_command "print_methods" "print methods of this theory" Keyword.diag
29.364 - (Scan.succeed (Toplevel.no_timing o IsarCmd.print_methods));
29.365 + (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_methods));
29.366
29.367 val _ =
29.368 Outer_Syntax.improper_command "print_antiquotations" "print antiquotations (global)" Keyword.diag
29.369 - (Scan.succeed (Toplevel.no_timing o IsarCmd.print_antiquotations));
29.370 + (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_antiquotations));
29.371
29.372 val _ =
29.373 Outer_Syntax.improper_command "thy_deps" "visualize theory dependencies"
29.374 - Keyword.diag (Scan.succeed (Toplevel.no_timing o IsarCmd.thy_deps));
29.375 + Keyword.diag (Scan.succeed (Toplevel.no_timing o Isar_Cmd.thy_deps));
29.376
29.377 val _ =
29.378 Outer_Syntax.improper_command "class_deps" "visualize class dependencies"
29.379 - Keyword.diag (Scan.succeed (Toplevel.no_timing o IsarCmd.class_deps));
29.380 + Keyword.diag (Scan.succeed (Toplevel.no_timing o Isar_Cmd.class_deps));
29.381
29.382 val _ =
29.383 Outer_Syntax.improper_command "thm_deps" "visualize theorem dependencies"
29.384 - Keyword.diag (Parse_Spec.xthms1 >> (Toplevel.no_timing oo IsarCmd.thm_deps));
29.385 + Keyword.diag (Parse_Spec.xthms1 >> (Toplevel.no_timing oo Isar_Cmd.thm_deps));
29.386
29.387 val _ =
29.388 Outer_Syntax.improper_command "print_binds" "print term bindings of proof context" Keyword.diag
29.389 - (Scan.succeed (Toplevel.no_timing o IsarCmd.print_binds));
29.390 + (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_binds));
29.391
29.392 val _ =
29.393 Outer_Syntax.improper_command "print_facts" "print facts of proof context" Keyword.diag
29.394 - (Scan.succeed (Toplevel.no_timing o IsarCmd.print_facts));
29.395 + (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_facts));
29.396
29.397 val _ =
29.398 Outer_Syntax.improper_command "print_cases" "print cases of proof context" Keyword.diag
29.399 - (Scan.succeed (Toplevel.no_timing o IsarCmd.print_cases));
29.400 + (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_cases));
29.401
29.402 val _ =
29.403 Outer_Syntax.improper_command "print_statement" "print theorems as long statements" Keyword.diag
29.404 - (opt_modes -- Parse_Spec.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_stmts));
29.405 + (opt_modes -- Parse_Spec.xthms1 >> (Toplevel.no_timing oo Isar_Cmd.print_stmts));
29.406
29.407 val _ =
29.408 Outer_Syntax.improper_command "thm" "print theorems" Keyword.diag
29.409 - (opt_modes -- Parse_Spec.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_thms));
29.410 + (opt_modes -- Parse_Spec.xthms1 >> (Toplevel.no_timing oo Isar_Cmd.print_thms));
29.411
29.412 val _ =
29.413 Outer_Syntax.improper_command "prf" "print proof terms of theorems" Keyword.diag
29.414 (opt_modes -- Scan.option Parse_Spec.xthms1
29.415 - >> (Toplevel.no_timing oo IsarCmd.print_prfs false));
29.416 + >> (Toplevel.no_timing oo Isar_Cmd.print_prfs false));
29.417
29.418 val _ =
29.419 Outer_Syntax.improper_command "full_prf" "print full proof terms of theorems" Keyword.diag
29.420 - (opt_modes -- Scan.option Parse_Spec.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_prfs true));
29.421 + (opt_modes -- Scan.option Parse_Spec.xthms1 >> (Toplevel.no_timing oo Isar_Cmd.print_prfs true));
29.422
29.423 val _ =
29.424 Outer_Syntax.improper_command "prop" "read and print proposition" Keyword.diag
29.425 - (opt_modes -- Parse.term >> (Toplevel.no_timing oo IsarCmd.print_prop));
29.426 + (opt_modes -- Parse.term >> (Toplevel.no_timing oo Isar_Cmd.print_prop));
29.427
29.428 val _ =
29.429 Outer_Syntax.improper_command "term" "read and print term" Keyword.diag
29.430 - (opt_modes -- Parse.term >> (Toplevel.no_timing oo IsarCmd.print_term));
29.431 + (opt_modes -- Parse.term >> (Toplevel.no_timing oo Isar_Cmd.print_term));
29.432
29.433 val _ =
29.434 Outer_Syntax.improper_command "typ" "read and print type" Keyword.diag
29.435 - (opt_modes -- Parse.typ >> (Toplevel.no_timing oo IsarCmd.print_type));
29.436 + (opt_modes -- Parse.typ >> (Toplevel.no_timing oo Isar_Cmd.print_type));
29.437
29.438 val _ =
29.439 Outer_Syntax.improper_command "print_codesetup" "print code generator setup" Keyword.diag
29.440 @@ -936,7 +936,7 @@
29.441 Outer_Syntax.improper_command "unused_thms" "find unused theorems" Keyword.diag
29.442 (Scan.option ((Scan.repeat1 (Scan.unless Parse.minus Parse.name) --| Parse.minus) --
29.443 Scan.option (Scan.repeat1 (Scan.unless Parse.minus Parse.name))) >>
29.444 - (Toplevel.no_timing oo IsarCmd.unused_thms));
29.445 + (Toplevel.no_timing oo Isar_Cmd.unused_thms));
29.446
29.447
29.448
29.449 @@ -944,54 +944,54 @@
29.450
29.451 val _ =
29.452 Outer_Syntax.improper_command "cd" "change current working directory" Keyword.diag
29.453 - (Parse.path >> (Toplevel.no_timing oo IsarCmd.cd));
29.454 + (Parse.path >> (Toplevel.no_timing oo Isar_Cmd.cd));
29.455
29.456 val _ =
29.457 Outer_Syntax.improper_command "pwd" "print current working directory" Keyword.diag
29.458 - (Scan.succeed (Toplevel.no_timing o IsarCmd.pwd));
29.459 + (Scan.succeed (Toplevel.no_timing o Isar_Cmd.pwd));
29.460
29.461 val _ =
29.462 Outer_Syntax.improper_command "use_thy" "use theory file" Keyword.diag
29.463 (Parse.name >> (fn name =>
29.464 - Toplevel.no_timing o Toplevel.imperative (fn () => ThyInfo.use_thy name)));
29.465 + Toplevel.no_timing o Toplevel.imperative (fn () => Thy_Info.use_thy name)));
29.466
29.467 val _ =
29.468 Outer_Syntax.improper_command "touch_thy" "outdate theory, including descendants" Keyword.diag
29.469 (Parse.name >> (fn name =>
29.470 - Toplevel.no_timing o Toplevel.imperative (fn () => ThyInfo.touch_thy name)));
29.471 + Toplevel.no_timing o Toplevel.imperative (fn () => Thy_Info.touch_thy name)));
29.472
29.473 val _ =
29.474 Outer_Syntax.improper_command "remove_thy" "remove theory from loader database" Keyword.diag
29.475 (Parse.name >> (fn name =>
29.476 - Toplevel.no_timing o Toplevel.imperative (fn () => ThyInfo.remove_thy name)));
29.477 + Toplevel.no_timing o Toplevel.imperative (fn () => Thy_Info.remove_thy name)));
29.478
29.479 val _ =
29.480 Outer_Syntax.improper_command "kill_thy" "kill theory -- try to remove from loader database"
29.481 Keyword.diag (Parse.name >> (fn name =>
29.482 - Toplevel.no_timing o Toplevel.imperative (fn () => ThyInfo.kill_thy name)));
29.483 + Toplevel.no_timing o Toplevel.imperative (fn () => Thy_Info.kill_thy name)));
29.484
29.485 val _ =
29.486 Outer_Syntax.improper_command "display_drafts" "display raw source files with symbols"
29.487 - Keyword.diag (Scan.repeat1 Parse.path >> (Toplevel.no_timing oo IsarCmd.display_drafts));
29.488 + Keyword.diag (Scan.repeat1 Parse.path >> (Toplevel.no_timing oo Isar_Cmd.display_drafts));
29.489
29.490 val _ =
29.491 Outer_Syntax.improper_command "print_drafts" "print raw source files with symbols"
29.492 - Keyword.diag (Scan.repeat1 Parse.path >> (Toplevel.no_timing oo IsarCmd.print_drafts));
29.493 + Keyword.diag (Scan.repeat1 Parse.path >> (Toplevel.no_timing oo Isar_Cmd.print_drafts));
29.494
29.495 val opt_limits =
29.496 Scan.option Parse.nat -- Scan.option (Parse.$$$ "," |-- Parse.!!! Parse.nat);
29.497
29.498 val _ =
29.499 Outer_Syntax.improper_command "pr" "print current proof state (if present)" Keyword.diag
29.500 - (opt_modes -- opt_limits >> (Toplevel.no_timing oo IsarCmd.pr));
29.501 + (opt_modes -- opt_limits >> (Toplevel.no_timing oo Isar_Cmd.pr));
29.502
29.503 val _ =
29.504 Outer_Syntax.improper_command "disable_pr" "disable printing of toplevel state" Keyword.diag
29.505 - (Scan.succeed (Toplevel.no_timing o IsarCmd.disable_pr));
29.506 + (Scan.succeed (Toplevel.no_timing o Isar_Cmd.disable_pr));
29.507
29.508 val _ =
29.509 Outer_Syntax.improper_command "enable_pr" "enable printing of toplevel state" Keyword.diag
29.510 - (Scan.succeed (Toplevel.no_timing o IsarCmd.enable_pr));
29.511 + (Scan.succeed (Toplevel.no_timing o Isar_Cmd.enable_pr));
29.512
29.513 val _ =
29.514 Outer_Syntax.improper_command "commit" "commit current session to ML database" Keyword.diag
29.515 @@ -999,11 +999,11 @@
29.516
29.517 val _ =
29.518 Outer_Syntax.improper_command "quit" "quit Isabelle" Keyword.control
29.519 - (Parse.opt_unit >> (Toplevel.no_timing oo K IsarCmd.quit));
29.520 + (Parse.opt_unit >> (Toplevel.no_timing oo K Isar_Cmd.quit));
29.521
29.522 val _ =
29.523 Outer_Syntax.improper_command "exit" "exit Isar loop" Keyword.control
29.524 - (Scan.succeed (Toplevel.no_timing o IsarCmd.exit));
29.525 + (Scan.succeed (Toplevel.no_timing o Isar_Cmd.exit));
29.526
29.527 end;
29.528
30.1 --- a/src/Pure/Isar/method.ML Mon May 31 19:36:13 2010 +0200
30.2 +++ b/src/Pure/Isar/method.ML Mon May 31 21:06:57 2010 +0200
30.3 @@ -271,15 +271,16 @@
30.4 val intros_tac = gen_intros_tac ALLGOALS;
30.5 val try_intros_tac = gen_intros_tac TRYALL;
30.6
30.7 +
30.8 (* ML tactics *)
30.9
30.10 -structure TacticData = Proof_Data
30.11 +structure ML_Tactic = Proof_Data
30.12 (
30.13 type T = thm list -> tactic;
30.14 fun init _ = undefined;
30.15 );
30.16
30.17 -val set_tactic = TacticData.put;
30.18 +val set_tactic = ML_Tactic.put;
30.19
30.20 fun ml_tactic (txt, pos) ctxt =
30.21 let
30.22 @@ -287,7 +288,7 @@
30.23 (ML_Context.expression pos
30.24 "fun tactic (facts: thm list) : tactic"
30.25 "Context.map_proof (Method.set_tactic tactic)" (ML_Lex.read pos txt));
30.26 - in Context.setmp_thread_data (SOME (Context.Proof ctxt)) (TacticData.get ctxt') end;
30.27 + in Context.setmp_thread_data (SOME (Context.Proof ctxt)) (ML_Tactic.get ctxt') end;
30.28
30.29 fun tactic txt ctxt = METHOD (ml_tactic txt ctxt);
30.30 fun raw_tactic txt ctxt = RAW_METHOD (ml_tactic txt ctxt);
31.1 --- a/src/Pure/Isar/object_logic.ML Mon May 31 19:36:13 2010 +0200
31.2 +++ b/src/Pure/Isar/object_logic.ML Mon May 31 21:06:57 2010 +0200
31.3 @@ -46,7 +46,7 @@
31.4 fun make_data (base_sort, judgment, atomize_rulify) =
31.5 Data {base_sort = base_sort, judgment = judgment, atomize_rulify = atomize_rulify};
31.6
31.7 -structure ObjectLogicData = Theory_Data
31.8 +structure Data = Theory_Data
31.9 (
31.10 type T = data;
31.11 val empty = make_data (NONE, NONE, ([], []));
31.12 @@ -63,10 +63,10 @@
31.13 (Thm.merge_thms (atomize1, atomize2), Thm.merge_thms (rulify1, rulify2)));
31.14 );
31.15
31.16 -fun map_data f = ObjectLogicData.map (fn (Data {base_sort, judgment, atomize_rulify}) =>
31.17 +fun map_data f = Data.map (fn (Data {base_sort, judgment, atomize_rulify}) =>
31.18 make_data (f (base_sort, judgment, atomize_rulify)));
31.19
31.20 -fun get_data thy = ObjectLogicData.get thy |> (fn Data args => args);
31.21 +fun get_data thy = Data.get thy |> (fn Data args => args);
31.22
31.23
31.24
32.1 --- a/src/Pure/Isar/outer_syntax.ML Mon May 31 19:36:13 2010 +0200
32.2 +++ b/src/Pure/Isar/outer_syntax.ML Mon May 31 21:06:57 2010 +0200
32.3 @@ -11,7 +11,7 @@
32.4 sig
32.5 val command: string -> string -> Keyword.T ->
32.6 (Toplevel.transition -> Toplevel.transition) parser -> unit
32.7 - val markup_command: ThyOutput.markup -> string -> string -> Keyword.T ->
32.8 + val markup_command: Thy_Output.markup -> string -> string -> Keyword.T ->
32.9 (Toplevel.transition -> Toplevel.transition) parser -> unit
32.10 val improper_command: string -> string -> Keyword.T ->
32.11 (Toplevel.transition -> Toplevel.transition) parser -> unit
32.12 @@ -43,7 +43,7 @@
32.13
32.14 datatype command = Command of
32.15 {comment: string,
32.16 - markup: ThyOutput.markup option,
32.17 + markup: Thy_Output.markup option,
32.18 int_only: bool,
32.19 parse: (Toplevel.transition -> Toplevel.transition) parser};
32.20
32.21 @@ -83,7 +83,7 @@
32.22 local
32.23
32.24 val global_commands = Unsynchronized.ref (Symtab.empty: command Symtab.table);
32.25 -val global_markups = Unsynchronized.ref ([]: (string * ThyOutput.markup) list);
32.26 +val global_markups = Unsynchronized.ref ([]: (string * Thy_Output.markup) list);
32.27
32.28 fun change_commands f = CRITICAL (fn () =>
32.29 (Unsynchronized.change global_commands f;
32.30 @@ -235,9 +235,9 @@
32.31
32.32 fun prepare_span commands span =
32.33 let
32.34 - val range_pos = Position.encode_range (ThySyntax.span_range span);
32.35 - val toks = ThySyntax.span_content span;
32.36 - val _ = List.app ThySyntax.report_token toks;
32.37 + val range_pos = Position.encode_range (Thy_Syntax.span_range span);
32.38 + val toks = Thy_Syntax.span_content span;
32.39 + val _ = List.app Thy_Syntax.report_token toks;
32.40 in
32.41 (case Source.exhaust (toplevel_source false NONE (K commands) (Source.of_list toks)) of
32.42 [tr] => (tr, true)
32.43 @@ -257,7 +257,7 @@
32.44
32.45 fun prepare_command pos str =
32.46 let val (lexs, commands) = get_syntax () in
32.47 - (case ThySyntax.parse_spans lexs pos str of
32.48 + (case Thy_Syntax.parse_spans lexs pos str of
32.49 [span] => #1 (prepare_span commands span)
32.50 | _ => Toplevel.malformed pos not_singleton)
32.51 end;
32.52 @@ -271,21 +271,21 @@
32.53
32.54 val _ = Present.init_theory name;
32.55
32.56 - val toks = Source.exhausted (ThySyntax.token_source lexs pos (Source.of_list text));
32.57 - val spans = Source.exhaust (ThySyntax.span_source toks);
32.58 - val _ = List.app ThySyntax.report_span spans;
32.59 - val units = Source.exhaust (ThySyntax.unit_source (Source.of_list spans))
32.60 + val toks = Source.exhausted (Thy_Syntax.token_source lexs pos (Source.of_list text));
32.61 + val spans = Source.exhaust (Thy_Syntax.span_source toks);
32.62 + val _ = List.app Thy_Syntax.report_span spans;
32.63 + val units = Source.exhaust (Thy_Syntax.unit_source (Source.of_list spans))
32.64 |> maps (prepare_unit commands);
32.65
32.66 val _ = Present.theory_source name
32.67 - (fn () => HTML.html_mode (implode o map ThySyntax.present_span) spans);
32.68 + (fn () => HTML.html_mode (implode o map Thy_Syntax.present_span) spans);
32.69
32.70 val _ = if time then writeln ("\n**** Starting theory " ^ quote name ^ " ****") else ();
32.71 val results = cond_timeit time "" (fn () => Toplevel.excursion units);
32.72 val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else ();
32.73
32.74 fun after_load () =
32.75 - ThyOutput.present_thy (#1 lexs) Keyword.command_tags is_markup (Lazy.force results) toks
32.76 + Thy_Output.present_thy (#1 lexs) Keyword.command_tags is_markup (Lazy.force results) toks
32.77 |> Buffer.content
32.78 |> Present.theory_output name;
32.79 in after_load end;
33.1 --- a/src/Pure/Isar/proof_context.ML Mon May 31 19:36:13 2010 +0200
33.2 +++ b/src/Pure/Isar/proof_context.ML Mon May 31 21:06:57 2010 +0200
33.3 @@ -193,7 +193,7 @@
33.4
33.5 val local_naming = Name_Space.default_naming |> Name_Space.add_path "local";
33.6
33.7 -structure ContextData = Proof_Data
33.8 +structure Data = Proof_Data
33.9 (
33.10 type T = ctxt;
33.11 fun init thy =
33.12 @@ -202,10 +202,10 @@
33.13 (Sign.consts_of thy, Sign.consts_of thy), Facts.empty, []);
33.14 );
33.15
33.16 -fun rep_context ctxt = ContextData.get ctxt |> (fn Ctxt args => args);
33.17 +fun rep_context ctxt = Data.get ctxt |> (fn Ctxt args => args);
33.18
33.19 fun map_context f =
33.20 - ContextData.map (fn Ctxt {mode, naming, syntax, tsig, consts, facts, cases} =>
33.21 + Data.map (fn Ctxt {mode, naming, syntax, tsig, consts, facts, cases} =>
33.22 make_ctxt (f (mode, naming, syntax, tsig, consts, facts, cases)));
33.23
33.24 fun set_mode mode = map_context (fn (_, naming, syntax, tsig, consts, facts, cases) =>
34.1 --- a/src/Pure/Isar/specification.ML Mon May 31 19:36:13 2010 +0200
34.2 +++ b/src/Pure/Isar/specification.ML Mon May 31 21:06:57 2010 +0200
34.3 @@ -361,7 +361,7 @@
34.4 #2 #> pair ths);
34.5 in ((prems, stmt, SOME facts), goal_ctxt) end);
34.6
34.7 -structure TheoremHook = Generic_Data
34.8 +structure Theorem_Hook = Generic_Data
34.9 (
34.10 type T = ((bool -> Proof.state -> Proof.state) * stamp) list;
34.11 val empty = [];
34.12 @@ -407,7 +407,7 @@
34.13 |> (case facts of NONE => I | SOME ths => Proof.refine_insert ths)
34.14 |> tap (fn state => not schematic andalso Proof.schematic_goal state andalso
34.15 error "Illegal schematic goal statement")
34.16 - |> Library.apply (map (fn (f, _) => f int) (rev (TheoremHook.get (Context.Proof goal_ctxt))))
34.17 + |> Library.apply (map (fn (f, _) => f int) (rev (Theorem_Hook.get (Context.Proof goal_ctxt))))
34.18 end;
34.19
34.20 in
34.21 @@ -418,7 +418,7 @@
34.22 val schematic_theorem = gen_theorem true (K I) Expression.cert_statement;
34.23 val schematic_theorem_cmd = gen_theorem true Attrib.intern_src Expression.read_statement;
34.24
34.25 -fun add_theorem_hook f = TheoremHook.map (cons (f, stamp ()));
34.26 +fun add_theorem_hook f = Theorem_Hook.map (cons (f, stamp ()));
34.27
34.28 end;
34.29
35.1 --- a/src/Pure/Isar/toplevel.ML Mon May 31 19:36:13 2010 +0200
35.2 +++ b/src/Pure/Isar/toplevel.ML Mon May 31 21:06:57 2010 +0200
35.3 @@ -238,7 +238,7 @@
35.4 |> Runtime.debugging
35.5 |> Runtime.toplevel_error
35.6 (fn exn => priority ("## INTERNAL ERROR ##\n" ^ ML_Compiler.exn_message exn))),
35.7 - SimpleThread.attributes interrupts);
35.8 + Simple_Thread.attributes interrupts);
35.9
35.10
35.11 (* node transactions -- maintaining stable checkpoints *)
35.12 @@ -638,7 +638,7 @@
35.13 fun run_command thy_name tr st =
35.14 (case
35.15 (case init_of tr of
35.16 - SOME name => Exn.capture (fn () => ThyLoad.check_name thy_name name) ()
35.17 + SOME name => Exn.capture (fn () => Thy_Load.check_name thy_name name) ()
35.18 | NONE => Exn.Result ()) of
35.19 Exn.Result () =>
35.20 (case transition true tr st of
36.1 --- a/src/Pure/ML/ml_antiquote.ML Mon May 31 19:36:13 2010 +0200
36.2 +++ b/src/Pure/ML/ml_antiquote.ML Mon May 31 21:06:57 2010 +0200
36.3 @@ -20,7 +20,7 @@
36.4
36.5 (* ML names *)
36.6
36.7 -structure NamesData = Proof_Data
36.8 +structure Names = Proof_Data
36.9 (
36.10 type T = Name.context;
36.11 fun init _ = ML_Syntax.reserved;
36.12 @@ -28,9 +28,9 @@
36.13
36.14 fun variant a ctxt =
36.15 let
36.16 - val names = NamesData.get ctxt;
36.17 + val names = Names.get ctxt;
36.18 val ([b], names') = Name.variants [a] names;
36.19 - val ctxt' = NamesData.put names' ctxt;
36.20 + val ctxt' = Names.put names' ctxt;
36.21 in (b, ctxt') end;
36.22
36.23
36.24 @@ -64,12 +64,12 @@
36.25 >> (fn name => ML_Syntax.atomic (ML_Syntax.make_binding name)));
36.26
36.27 val _ = value "theory"
36.28 - (Scan.lift Args.name >> (fn name => "ThyInfo.get_theory " ^ ML_Syntax.print_string name)
36.29 + (Scan.lift Args.name >> (fn name => "Thy_Info.get_theory " ^ ML_Syntax.print_string name)
36.30 || Scan.succeed "ML_Context.the_global_context ()");
36.31
36.32 val _ = value "theory_ref"
36.33 (Scan.lift Args.name >> (fn name =>
36.34 - "Theory.check_thy (ThyInfo.theory " ^ ML_Syntax.print_string name ^ ")")
36.35 + "Theory.check_thy (Thy_Info.theory " ^ ML_Syntax.print_string name ^ ")")
36.36 || Scan.succeed "Theory.check_thy (ML_Context.the_global_context ())");
36.37
36.38 val _ = value "context" (Scan.succeed "ML_Context.the_local_context ()");
37.1 --- a/src/Pure/ML/ml_thms.ML Mon May 31 19:36:13 2010 +0200
37.2 +++ b/src/Pure/ML/ml_thms.ML Mon May 31 21:06:57 2010 +0200
37.3 @@ -15,15 +15,15 @@
37.4
37.5 (* auxiliary facts table *)
37.6
37.7 -structure AuxFacts = Proof_Data
37.8 +structure Aux_Facts = Proof_Data
37.9 (
37.10 type T = thm list Inttab.table;
37.11 fun init _ = Inttab.empty;
37.12 );
37.13
37.14 -val put_thms = AuxFacts.map o Inttab.update;
37.15 +val put_thms = Aux_Facts.map o Inttab.update;
37.16
37.17 -fun the_thms ctxt name = the (Inttab.lookup (AuxFacts.get ctxt) name);
37.18 +fun the_thms ctxt name = the (Inttab.lookup (Aux_Facts.get ctxt) name);
37.19 fun the_thm ctxt name = the_single (the_thms ctxt name);
37.20
37.21 fun thm_bind kind a i =
38.1 --- a/src/Pure/ProofGeneral/pgip_isabelle.ML Mon May 31 19:36:13 2010 +0200
38.2 +++ b/src/Pure/ProofGeneral/pgip_isabelle.ML Mon May 31 21:06:57 2010 +0200
38.3 @@ -80,7 +80,7 @@
38.4 NONE => (NONE, NONE)
38.5 | SOME fname =>
38.6 let val path = Path.explode fname in
38.7 - case ThyLoad.check_file Path.current path of
38.8 + case Thy_Load.check_file Path.current path of
38.9 SOME _ => (SOME (PgipTypes.pgipurl_of_path path), NONE)
38.10 | NONE => (NONE, SOME fname)
38.11 end);
39.1 --- a/src/Pure/ProofGeneral/pgip_parser.ML Mon May 31 19:36:13 2010 +0200
39.2 +++ b/src/Pure/ProofGeneral/pgip_parser.ML Mon May 31 21:06:57 2010 +0200
39.3 @@ -91,18 +91,18 @@
39.4
39.5 fun parse_span span =
39.6 let
39.7 - val kind = ThySyntax.span_kind span;
39.8 - val toks = ThySyntax.span_content span;
39.9 - val text = implode (map (Print_Mode.setmp [] ThySyntax.present_token) toks);
39.10 + val kind = Thy_Syntax.span_kind span;
39.11 + val toks = Thy_Syntax.span_content span;
39.12 + val text = implode (map (Print_Mode.setmp [] Thy_Syntax.present_token) toks);
39.13 in
39.14 (case kind of
39.15 - ThySyntax.Command name => parse_command name text
39.16 - | ThySyntax.Ignored => [D.Whitespace {text = text}]
39.17 - | ThySyntax.Malformed => [D.Unparseable {text = text}])
39.18 + Thy_Syntax.Command name => parse_command name text
39.19 + | Thy_Syntax.Ignored => [D.Whitespace {text = text}]
39.20 + | Thy_Syntax.Malformed => [D.Unparseable {text = text}])
39.21 end;
39.22
39.23
39.24 fun pgip_parser pos str =
39.25 - maps parse_span (ThySyntax.parse_spans (Keyword.get_lexicons ()) pos str);
39.26 + maps parse_span (Thy_Syntax.parse_spans (Keyword.get_lexicons ()) pos str);
39.27
39.28 end;
40.1 --- a/src/Pure/ProofGeneral/proof_general_emacs.ML Mon May 31 19:36:13 2010 +0200
40.2 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Mon May 31 21:06:57 2010 +0200
40.3 @@ -113,15 +113,15 @@
40.4 local
40.5
40.6 fun trace_action action name =
40.7 - if action = ThyInfo.Update then
40.8 - List.app tell_file_loaded (ThyInfo.loaded_files name)
40.9 - else if action = ThyInfo.Outdate orelse action = ThyInfo.Remove then
40.10 - List.app tell_file_retracted (ThyInfo.loaded_files name)
40.11 + if action = Thy_Info.Update then
40.12 + List.app tell_file_loaded (Thy_Info.loaded_files name)
40.13 + else if action = Thy_Info.Outdate orelse action = Thy_Info.Remove then
40.14 + List.app tell_file_retracted (Thy_Info.loaded_files name)
40.15 else ();
40.16
40.17 in
40.18 - fun setup_thy_loader () = ThyInfo.add_hook trace_action;
40.19 - fun sync_thy_loader () = List.app (trace_action ThyInfo.Update) (ThyInfo.get_names ());
40.20 + fun setup_thy_loader () = Thy_Info.add_hook trace_action;
40.21 + fun sync_thy_loader () = List.app (trace_action Thy_Info.Update) (Thy_Info.get_names ());
40.22 end;
40.23
40.24
40.25 @@ -130,19 +130,19 @@
40.26 (*liberal low-level version*)
40.27 val thy_name = perhaps (try (unsuffix ".thy")) o List.last o space_explode "/";
40.28
40.29 -val inform_file_retracted = ThyInfo.if_known_thy ThyInfo.remove_thy o thy_name;
40.30 +val inform_file_retracted = Thy_Info.if_known_thy Thy_Info.remove_thy o thy_name;
40.31
40.32 fun inform_file_processed file =
40.33 let
40.34 val name = thy_name file;
40.35 val _ = name = "" andalso error ("Bad file name: " ^ quote file);
40.36 val _ =
40.37 - if ThyInfo.check_known_thy name then
40.38 + if Thy_Info.check_known_thy name then
40.39 (Isar.>> (Toplevel.commit_exit Position.none);
40.40 - ThyInfo.touch_child_thys name; ThyInfo.register_thy name)
40.41 + Thy_Info.touch_child_thys name; Thy_Info.register_thy name)
40.42 handle ERROR msg =>
40.43 (warning (cat_lines ["Failed to register theory: " ^ quote name, msg]);
40.44 - tell_file_retracted (ThyLoad.thy_path name))
40.45 + tell_file_retracted (Thy_Load.thy_path name))
40.46 else ();
40.47 val _ = Isar.init ();
40.48 in () end;
41.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML Mon May 31 19:36:13 2010 +0200
41.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Mon May 31 21:06:57 2010 +0200
41.3 @@ -198,18 +198,18 @@
41.4 operations).
41.5 *)
41.6 fun trace_action action name =
41.7 - if action = ThyInfo.Update then
41.8 - List.app (tell_file_loaded true) (ThyInfo.loaded_files name)
41.9 - else if action = ThyInfo.Outdate then
41.10 - List.app (tell_file_outdated true) (ThyInfo.loaded_files name)
41.11 - else if action = ThyInfo.Remove then
41.12 - List.app (tell_file_retracted true) (ThyInfo.loaded_files name)
41.13 + if action = Thy_Info.Update then
41.14 + List.app (tell_file_loaded true) (Thy_Info.loaded_files name)
41.15 + else if action = Thy_Info.Outdate then
41.16 + List.app (tell_file_outdated true) (Thy_Info.loaded_files name)
41.17 + else if action = Thy_Info.Remove then
41.18 + List.app (tell_file_retracted true) (Thy_Info.loaded_files name)
41.19 else ()
41.20
41.21
41.22 in
41.23 - fun setup_thy_loader () = ThyInfo.add_hook trace_action;
41.24 - fun sync_thy_loader () = List.app (trace_action ThyInfo.Update) (ThyInfo.get_names ());
41.25 + fun setup_thy_loader () = Thy_Info.add_hook trace_action;
41.26 + fun sync_thy_loader () = List.app (trace_action Thy_Info.Update) (Thy_Info.get_names ());
41.27 end;
41.28
41.29
41.30 @@ -217,14 +217,14 @@
41.31
41.32 val thy_name = Path.implode o #1 o Path.split_ext o Path.base;
41.33
41.34 -val inform_file_retracted = ThyInfo.if_known_thy ThyInfo.remove_thy o thy_name;
41.35 -val inform_file_processed = ThyInfo.if_known_thy ThyInfo.touch_child_thys o thy_name;
41.36 +val inform_file_retracted = Thy_Info.if_known_thy Thy_Info.remove_thy o thy_name;
41.37 +val inform_file_processed = Thy_Info.if_known_thy Thy_Info.touch_child_thys o thy_name;
41.38
41.39 fun proper_inform_file_processed path state =
41.40 let val name = thy_name path in
41.41 - if Toplevel.is_toplevel state andalso ThyInfo.known_thy name then
41.42 - (ThyInfo.touch_child_thys name;
41.43 - ThyInfo.register_thy name handle ERROR msg =>
41.44 + if Toplevel.is_toplevel state andalso Thy_Info.known_thy name then
41.45 + (Thy_Info.touch_child_thys name;
41.46 + Thy_Info.register_thy name handle ERROR msg =>
41.47 (warning (cat_lines [msg, "Failed to register theory: " ^ quote name]);
41.48 tell_file_retracted true (Path.base path)))
41.49 else raise Toplevel.UNDEF
41.50 @@ -522,7 +522,7 @@
41.51 local
41.52
41.53 fun theory_facts name =
41.54 - let val thy = ThyInfo.get_theory name
41.55 + let val thy = Thy_Info.get_theory name
41.56 in (map PureThy.facts_of (Theory.parents_of thy), PureThy.facts_of thy) end;
41.57
41.58 fun thms_of_thy name = map fst (theory_facts name |-> Facts.extern_static);
41.59 @@ -556,13 +556,13 @@
41.60 in
41.61 case (thyname,objtype) of
41.62 (NONE, NONE) =>
41.63 - setids (idtable ObjFile NONE (ThyInfo.get_names())) (*FIXME: uris*)
41.64 + setids (idtable ObjFile NONE (Thy_Info.get_names())) (*FIXME: uris*)
41.65 | (NONE, SOME ObjFile) =>
41.66 - setids (idtable ObjFile NONE (ThyInfo.get_names())) (*FIXME: uris*)
41.67 + setids (idtable ObjFile NONE (Thy_Info.get_names())) (*FIXME: uris*)
41.68 | (SOME fi, SOME ObjFile) =>
41.69 setids (idtable ObjTheory (SOME fi) [fi]) (* TODO: check exists *)
41.70 | (NONE, SOME ObjTheory) =>
41.71 - setids (idtable ObjTheory NONE (ThyInfo.get_names()))
41.72 + setids (idtable ObjTheory NONE (Thy_Info.get_names()))
41.73 | (SOME thy, SOME ObjTheory) =>
41.74 setids (idtable ObjTheory (SOME thy) (subthys_of_thy thy))
41.75 | (SOME thy, SOME ObjTheorem) =>
41.76 @@ -571,9 +571,9 @@
41.77 (* A large query, but not unreasonable. ~5000 results for HOL.*)
41.78 (* Several setids should be allowed, but Eclipse code is currently broken:
41.79 List.app (fn thy => setids (idtable ObjTheorem (SOME thy) (subthms_of_thy thy)))
41.80 - (ThyInfo.get_names()) *)
41.81 + (Thy_Info.get_names()) *)
41.82 setids (idtable ObjTheorem NONE (* this one gives ~7000 for HOL *)
41.83 - (maps qualified_thms_of_thy (ThyInfo.get_names())))
41.84 + (maps qualified_thms_of_thy (Thy_Info.get_names())))
41.85 | _ => warning ("askids: ignored argument combination")
41.86 end
41.87
41.88 @@ -592,14 +592,14 @@
41.89
41.90 fun filerefs f =
41.91 let val thy = thy_name f
41.92 - val filerefs = #uses (ThyLoad.deps_thy (Path.dir f) thy)
41.93 + val filerefs = #uses (Thy_Load.deps_thy (Path.dir f) thy)
41.94 in
41.95 issue_pgip (Setrefs {url=url, thyname=NONE, objtype=SOME PgipTypes.ObjFile,
41.96 name=NONE, idtables=[], fileurls=filerefs})
41.97 end
41.98
41.99 fun thyrefs thy =
41.100 - let val thyrefs = #imports (ThyLoad.deps_thy Path.current thy)
41.101 + let val thyrefs = #imports (Thy_Load.deps_thy Path.current thy)
41.102 in
41.103 issue_pgip (Setrefs {url=url, thyname=thyname, objtype=SOME PgipTypes.ObjTheory,
41.104 name=NONE, idtables=[{context=NONE, objtype=PgipTypes.ObjTheory,
41.105 @@ -642,7 +642,7 @@
41.106 fun splitthy id =
41.107 let val comps = Long_Name.explode id
41.108 in case comps of
41.109 - (thy::(rest as _::_)) => (ThyInfo.get_theory thy, space_implode "." rest)
41.110 + (thy::(rest as _::_)) => (Thy_Info.get_theory thy, space_implode "." rest)
41.111 | [plainid] => (topthy(),plainid)
41.112 | _ => raise Toplevel.UNDEF (* assert false *)
41.113 end
41.114 @@ -659,8 +659,8 @@
41.115 val string_of_thy = Pretty.string_of o Proof_Display.pretty_full_theory false
41.116 in
41.117 case (thyname, objtype) of
41.118 - (_, ObjTheory) => idvalue [string_of_thy (ThyInfo.get_theory name)]
41.119 - | (SOME thy, ObjTheorem) => idvalue (strings_of_thm (ThyInfo.get_theory thy, name))
41.120 + (_, ObjTheory) => idvalue [string_of_thy (Thy_Info.get_theory name)]
41.121 + | (SOME thy, ObjTheorem) => idvalue (strings_of_thm (Thy_Info.get_theory thy, name))
41.122 | (NONE, ObjTheorem) => idvalue (strings_of_thm (splitthy name))
41.123 | (_, ot) => error ("Cannot show objects of type "^(PgipTypes.name_of_objtype ot))
41.124 end
41.125 @@ -785,8 +785,8 @@
41.126 in
41.127 (case (!current_working_dir) of
41.128 NONE => ()
41.129 - | SOME dir => ThyLoad.del_path dir;
41.130 - ThyLoad.add_path newdir;
41.131 + | SOME dir => Thy_Load.del_path dir;
41.132 + Thy_Load.add_path newdir;
41.133 current_working_dir := SOME newdir)
41.134 end
41.135 end
41.136 @@ -806,7 +806,7 @@
41.137 val filedir = Path.dir filepath
41.138 val thy_name = Path.implode o #1 o Path.split_ext o Path.base
41.139 val openfile_retract = Output.no_warnings_CRITICAL
41.140 - (ThyInfo.if_known_thy ThyInfo.remove_thy) o thy_name;
41.141 + (Thy_Info.if_known_thy Thy_Info.remove_thy) o thy_name;
41.142 in
41.143 case !currently_open_file of
41.144 SOME f => raise PGIP ("<openfile> when a file is already open!\nCurrently open file: " ^
41.145 @@ -856,7 +856,7 @@
41.146 (* TODO: next should be in thy loader, here just for testing *)
41.147 let
41.148 val name = thy_name url
41.149 - in List.app (tell_file_retracted false) (ThyInfo.loaded_files name) end;
41.150 + in List.app (tell_file_retracted false) (Thy_Info.loaded_files name) end;
41.151 inform_file_retracted url)
41.152 end
41.153
42.1 --- a/src/Pure/ROOT.ML Mon May 31 19:36:13 2010 +0200
42.2 +++ b/src/Pure/ROOT.ML Mon May 31 21:06:57 2010 +0200
42.3 @@ -299,18 +299,15 @@
42.4 struct
42.5
42.6 structure OuterKeyword = Keyword;
42.7 -
42.8 -structure OuterLex =
42.9 -struct
42.10 - open Token;
42.11 - type token = T;
42.12 -end;
42.13 -
42.14 +structure OuterLex = struct open Token type token = T end;
42.15 structure OuterParse = Parse;
42.16 structure OuterSyntax = Outer_Syntax;
42.17 +structure PrintMode = Print_Mode;
42.18 structure SpecParse = Parse_Spec;
42.19 +structure ThyInfo = Thy_Info;
42.20 +structure ThyLoad = Thy_Load;
42.21 +structure ThyOutput = Thy_Output;
42.22 structure TypeInfer = Type_Infer;
42.23 -structure PrintMode = Print_Mode;
42.24
42.25 end;
42.26
43.1 --- a/src/Pure/Syntax/mixfix.ML Mon May 31 19:36:13 2010 +0200
43.2 +++ b/src/Pure/Syntax/mixfix.ML Mon May 31 21:06:57 2010 +0200
43.3 @@ -31,8 +31,8 @@
43.4 signature MIXFIX =
43.5 sig
43.6 include MIXFIX1
43.7 - val syn_ext_types: (string * typ * mixfix) list -> SynExt.syn_ext
43.8 - val syn_ext_consts: (string -> bool) -> (string * typ * mixfix) list -> SynExt.syn_ext
43.9 + val syn_ext_types: (string * typ * mixfix) list -> Syn_Ext.syn_ext
43.10 + val syn_ext_consts: (string -> bool) -> (string * typ * mixfix) list -> Syn_Ext.syn_ext
43.11 end;
43.12
43.13 structure Mixfix: MIXFIX =
43.14 @@ -83,11 +83,11 @@
43.15 (* syntax specifications *)
43.16
43.17 fun mixfix_args NoSyn = 0
43.18 - | mixfix_args (Mixfix (sy, _, _)) = SynExt.mfix_args sy
43.19 - | mixfix_args (Delimfix sy) = SynExt.mfix_args sy
43.20 - | mixfix_args (Infix (sy, _)) = 2 + SynExt.mfix_args sy
43.21 - | mixfix_args (Infixl (sy, _)) = 2 + SynExt.mfix_args sy
43.22 - | mixfix_args (Infixr (sy, _)) = 2 + SynExt.mfix_args sy
43.23 + | mixfix_args (Mixfix (sy, _, _)) = Syn_Ext.mfix_args sy
43.24 + | mixfix_args (Delimfix sy) = Syn_Ext.mfix_args sy
43.25 + | mixfix_args (Infix (sy, _)) = 2 + Syn_Ext.mfix_args sy
43.26 + | mixfix_args (Infixl (sy, _)) = 2 + Syn_Ext.mfix_args sy
43.27 + | mixfix_args (Infixr (sy, _)) = 2 + Syn_Ext.mfix_args sy
43.28 | mixfix_args (Binder _) = 1
43.29 | mixfix_args Structure = 0;
43.30
43.31 @@ -97,29 +97,29 @@
43.32
43.33 (* syn_ext_types *)
43.34
43.35 -fun make_type n = replicate n SynExt.typeT ---> SynExt.typeT;
43.36 +fun make_type n = replicate n Syn_Ext.typeT ---> Syn_Ext.typeT;
43.37
43.38 fun syn_ext_types type_decls =
43.39 let
43.40 - fun mk_infix sy ty t p1 p2 p3 = SynExt.Mfix ("(_ " ^ sy ^ "/ _)", ty, t, [p1, p2], p3);
43.41 + fun mk_infix sy ty t p1 p2 p3 = Syn_Ext.Mfix ("(_ " ^ sy ^ "/ _)", ty, t, [p1, p2], p3);
43.42
43.43 fun mfix_of (_, _, NoSyn) = NONE
43.44 - | mfix_of (t, ty, Mixfix (sy, ps, p)) = SOME (SynExt.Mfix (sy, ty, t, ps, p))
43.45 - | mfix_of (t, ty, Delimfix sy) = SOME (SynExt.Mfix (sy, ty, t, [], SynExt.max_pri))
43.46 + | mfix_of (t, ty, Mixfix (sy, ps, p)) = SOME (Syn_Ext.Mfix (sy, ty, t, ps, p))
43.47 + | mfix_of (t, ty, Delimfix sy) = SOME (Syn_Ext.Mfix (sy, ty, t, [], Syn_Ext.max_pri))
43.48 | mfix_of (t, ty, Infix (sy, p)) = SOME (mk_infix sy ty t (p + 1) (p + 1) p)
43.49 | mfix_of (t, ty, Infixl (sy, p)) = SOME (mk_infix sy ty t p (p + 1) p)
43.50 | mfix_of (t, ty, Infixr (sy, p)) = SOME (mk_infix sy ty t (p + 1) p p)
43.51 | mfix_of (t, _, _) = error ("Bad mixfix declaration for " ^ quote t); (* FIXME printable t (!?) *)
43.52
43.53 - fun check_args (_, ty, _) (SOME (mfix as SynExt.Mfix (sy, _, _, _, _))) =
43.54 - if length (Term.binder_types ty) = SynExt.mfix_args sy then ()
43.55 - else SynExt.err_in_mfix "Bad number of type constructor arguments" mfix
43.56 + fun check_args (_, ty, _) (SOME (mfix as Syn_Ext.Mfix (sy, _, _, _, _))) =
43.57 + if length (Term.binder_types ty) = Syn_Ext.mfix_args sy then ()
43.58 + else Syn_Ext.err_in_mfix "Bad number of type constructor arguments" mfix
43.59 | check_args _ NONE = ();
43.60
43.61 val mfix = map mfix_of type_decls;
43.62 val _ = map2 check_args type_decls mfix;
43.63 val xconsts = map #1 type_decls;
43.64 - in SynExt.syn_ext (map_filter I mfix) xconsts ([], [], [], []) [] ([], []) end;
43.65 + in Syn_Ext.syn_ext (map_filter I mfix) xconsts ([], [], [], []) [] ([], []) end;
43.66
43.67
43.68 (* syn_ext_consts *)
43.69 @@ -130,21 +130,21 @@
43.70 fun syn_ext_consts is_logtype const_decls =
43.71 let
43.72 fun mk_infix sy ty c p1 p2 p3 =
43.73 - [SynExt.Mfix ("op " ^ sy, ty, c, [], SynExt.max_pri),
43.74 - SynExt.Mfix ("(_ " ^ sy ^ "/ _)", ty, c, [p1, p2], p3)];
43.75 + [Syn_Ext.Mfix ("op " ^ sy, ty, c, [], Syn_Ext.max_pri),
43.76 + Syn_Ext.Mfix ("(_ " ^ sy ^ "/ _)", ty, c, [p1, p2], p3)];
43.77
43.78 fun binder_typ _ (Type ("fun", [Type ("fun", [_, ty2]), ty3])) =
43.79 [Type ("idts", []), ty2] ---> ty3
43.80 | binder_typ c _ = error ("Bad type of binder: " ^ quote c);
43.81
43.82 fun mfix_of (_, _, NoSyn) = []
43.83 - | mfix_of (c, ty, Mixfix (sy, ps, p)) = [SynExt.Mfix (sy, ty, c, ps, p)]
43.84 - | mfix_of (c, ty, Delimfix sy) = [SynExt.Mfix (sy, ty, c, [], SynExt.max_pri)]
43.85 + | mfix_of (c, ty, Mixfix (sy, ps, p)) = [Syn_Ext.Mfix (sy, ty, c, ps, p)]
43.86 + | mfix_of (c, ty, Delimfix sy) = [Syn_Ext.Mfix (sy, ty, c, [], Syn_Ext.max_pri)]
43.87 | mfix_of (c, ty, Infix (sy, p)) = mk_infix sy ty c (p + 1) (p + 1) p
43.88 | mfix_of (c, ty, Infixl (sy, p)) = mk_infix sy ty c p (p + 1) p
43.89 | mfix_of (c, ty, Infixr (sy, p)) = mk_infix sy ty c (p + 1) p p
43.90 | mfix_of (c, ty, Binder (sy, p, q)) =
43.91 - [SynExt.Mfix ("(3" ^ sy ^ "_./ _)", binder_typ c ty, (binder_name c), [0, p], q)]
43.92 + [Syn_Ext.Mfix ("(3" ^ sy ^ "_./ _)", binder_typ c ty, (binder_name c), [0, p], q)]
43.93 | mfix_of (c, _, _) = error ("Bad mixfix declaration for " ^ quote c); (* FIXME printable c (!?) *)
43.94
43.95 fun binder (c, _, Binder _) = SOME (binder_name c, c)
43.96 @@ -154,12 +154,12 @@
43.97 val xconsts = map #1 const_decls;
43.98 val binders = map_filter binder const_decls;
43.99 val binder_trs = binders
43.100 - |> map (SynExt.stamp_trfun binder_stamp o apsnd K o SynTrans.mk_binder_tr);
43.101 + |> map (Syn_Ext.stamp_trfun binder_stamp o apsnd K o Syn_Trans.mk_binder_tr);
43.102 val binder_trs' = binders
43.103 - |> map (SynExt.stamp_trfun binder_stamp o
43.104 - apsnd (K o SynTrans.non_typed_tr') o SynTrans.mk_binder_tr' o swap);
43.105 + |> map (Syn_Ext.stamp_trfun binder_stamp o
43.106 + apsnd (K o Syn_Trans.non_typed_tr') o Syn_Trans.mk_binder_tr' o swap);
43.107 in
43.108 - SynExt.syn_ext' true is_logtype
43.109 + Syn_Ext.syn_ext' true is_logtype
43.110 mfix xconsts ([], binder_trs, binder_trs', []) [] ([], [])
43.111 end;
43.112
44.1 --- a/src/Pure/Syntax/parser.ML Mon May 31 19:36:13 2010 +0200
44.2 +++ b/src/Pure/Syntax/parser.ML Mon May 31 21:06:57 2010 +0200
44.3 @@ -8,8 +8,8 @@
44.4 sig
44.5 type gram
44.6 val empty_gram: gram
44.7 - val extend_gram: gram -> SynExt.xprod list -> gram
44.8 - val make_gram: SynExt.xprod list -> gram
44.9 + val extend_gram: gram -> Syn_Ext.xprod list -> gram
44.10 + val make_gram: Syn_Ext.xprod list -> gram
44.11 val merge_grams: gram -> gram -> gram
44.12 val pretty_gram: gram -> Pretty.T list
44.13 datatype parsetree =
44.14 @@ -23,7 +23,7 @@
44.15 structure Parser: PARSER =
44.16 struct
44.17
44.18 -open Lexicon SynExt;
44.19 +open Lexicon Syn_Ext;
44.20
44.21
44.22 (** datatype gram **)
45.1 --- a/src/Pure/Syntax/printer.ML Mon May 31 19:36:13 2010 +0200
45.2 +++ b/src/Pure/Syntax/printer.ML Mon May 31 21:06:57 2010 +0200
45.3 @@ -26,8 +26,8 @@
45.4 (string -> (Proof.context -> bool -> typ -> term list -> term) list) -> term -> Ast.ast
45.5 type prtabs
45.6 val empty_prtabs: prtabs
45.7 - val update_prtabs: string -> SynExt.xprod list -> prtabs -> prtabs
45.8 - val remove_prtabs: string -> SynExt.xprod list -> prtabs -> prtabs
45.9 + val update_prtabs: string -> Syn_Ext.xprod list -> prtabs -> prtabs
45.10 + val remove_prtabs: string -> Syn_Ext.xprod list -> prtabs -> prtabs
45.11 val merge_prtabs: prtabs -> prtabs -> prtabs
45.12 val pretty_term_ast: {extern_class: string -> xstring, extern_type: string -> xstring,
45.13 extern_const: string -> xstring} -> Proof.context -> bool -> prtabs ->
45.14 @@ -101,8 +101,8 @@
45.15 handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args);
45.16 in ast_of tm end;
45.17
45.18 -fun sort_to_ast ctxt trf S = ast_of_termT ctxt trf (TypeExt.term_of_sort S);
45.19 -fun typ_to_ast ctxt trf T = ast_of_termT ctxt trf (TypeExt.term_of_typ (! show_sorts) T);
45.20 +fun sort_to_ast ctxt trf S = ast_of_termT ctxt trf (Type_Ext.term_of_sort S);
45.21 +fun typ_to_ast ctxt trf T = ast_of_termT ctxt trf (Type_Ext.term_of_typ (! show_sorts) T);
45.22
45.23
45.24
45.25 @@ -114,7 +114,7 @@
45.26 val {structs, fixes} = idents;
45.27
45.28 fun mark_atoms ((t as Const (c, T)) $ u) =
45.29 - if member (op =) SynExt.standard_token_markers c
45.30 + if member (op =) Syn_Ext.standard_token_markers c
45.31 then t $ u else mark_atoms t $ mark_atoms u
45.32 | mark_atoms (t $ u) = mark_atoms t $ mark_atoms u
45.33 | mark_atoms (Abs (x, T, t)) = Abs (x, T, mark_atoms t)
45.34 @@ -130,7 +130,7 @@
45.35 else Lexicon.const "_free" $ t
45.36 end
45.37 | mark_atoms (t as Var (xi, T)) =
45.38 - if xi = SynExt.dddot_indexname then Const ("_DDDOT", T)
45.39 + if xi = Syn_Ext.dddot_indexname then Const ("_DDDOT", T)
45.40 else Lexicon.const "_var" $ t
45.41 | mark_atoms a = a;
45.42
45.43 @@ -155,7 +155,7 @@
45.44
45.45 fun ast_of tm =
45.46 (case strip_comb tm of
45.47 - (t as Abs _, ts) => Ast.mk_appl (ast_of (SynTrans.abs_tr' t)) (map ast_of ts)
45.48 + (t as Abs _, ts) => Ast.mk_appl (ast_of (Syn_Trans.abs_tr' t)) (map ast_of ts)
45.49 | ((c as Const ("_free", _)), Free (x, T) :: ts) =>
45.50 Ast.mk_appl (constrain (c $ Lexicon.free x) T) (map ast_of ts)
45.51 | ((c as Const ("_var", _)), Var (xi, T) :: ts) =>
45.52 @@ -176,12 +176,12 @@
45.53
45.54 and constrain t T =
45.55 if show_types andalso T <> dummyT then
45.56 - Ast.Appl [Ast.Constant SynExt.constrainC, simple_ast_of t,
45.57 - ast_of_termT ctxt trf (TypeExt.term_of_typ show_sorts T)]
45.58 + Ast.Appl [Ast.Constant Syn_Ext.constrainC, simple_ast_of t,
45.59 + ast_of_termT ctxt trf (Type_Ext.term_of_typ show_sorts T)]
45.60 else simple_ast_of t;
45.61 in
45.62 tm
45.63 - |> SynTrans.prop_tr'
45.64 + |> Syn_Trans.prop_tr'
45.65 |> show_types ? (#1 o prune_typs o rpair [])
45.66 |> mark_atoms
45.67 |> ast_of
45.68 @@ -211,29 +211,29 @@
45.69
45.70 (* xprod_to_fmt *)
45.71
45.72 -fun xprod_to_fmt (SynExt.XProd (_, _, "", _)) = NONE
45.73 - | xprod_to_fmt (SynExt.XProd (_, xsymbs, const, pri)) =
45.74 +fun xprod_to_fmt (Syn_Ext.XProd (_, _, "", _)) = NONE
45.75 + | xprod_to_fmt (Syn_Ext.XProd (_, xsymbs, const, pri)) =
45.76 let
45.77 fun arg (s, p) =
45.78 (if s = "type" then TypArg else Arg)
45.79 - (if Lexicon.is_terminal s then SynExt.max_pri else p);
45.80 + (if Lexicon.is_terminal s then Syn_Ext.max_pri else p);
45.81
45.82 - fun xsyms_to_syms (SynExt.Delim s :: xsyms) =
45.83 + fun xsyms_to_syms (Syn_Ext.Delim s :: xsyms) =
45.84 apfst (cons (String s)) (xsyms_to_syms xsyms)
45.85 - | xsyms_to_syms (SynExt.Argument s_p :: xsyms) =
45.86 + | xsyms_to_syms (Syn_Ext.Argument s_p :: xsyms) =
45.87 apfst (cons (arg s_p)) (xsyms_to_syms xsyms)
45.88 - | xsyms_to_syms (SynExt.Space s :: xsyms) =
45.89 + | xsyms_to_syms (Syn_Ext.Space s :: xsyms) =
45.90 apfst (cons (Space s)) (xsyms_to_syms xsyms)
45.91 - | xsyms_to_syms (SynExt.Bg i :: xsyms) =
45.92 + | xsyms_to_syms (Syn_Ext.Bg i :: xsyms) =
45.93 let
45.94 val (bsyms, xsyms') = xsyms_to_syms xsyms;
45.95 val (syms, xsyms'') = xsyms_to_syms xsyms';
45.96 in
45.97 (Block (i, bsyms) :: syms, xsyms'')
45.98 end
45.99 - | xsyms_to_syms (SynExt.Brk i :: xsyms) =
45.100 + | xsyms_to_syms (Syn_Ext.Brk i :: xsyms) =
45.101 apfst (cons (Break i)) (xsyms_to_syms xsyms)
45.102 - | xsyms_to_syms (SynExt.En :: xsyms) = ([], xsyms)
45.103 + | xsyms_to_syms (Syn_Ext.En :: xsyms) = ([], xsyms)
45.104 | xsyms_to_syms [] = ([], []);
45.105
45.106 fun nargs (Arg _ :: syms) = nargs syms + 1
45.107 @@ -263,7 +263,7 @@
45.108 fun remove_prtabs mode xprods prtabs =
45.109 let
45.110 val tab = mode_tab prtabs mode;
45.111 - val fmts = map_filter (fn xprod as SynExt.XProd (_, _, c, _) =>
45.112 + val fmts = map_filter (fn xprod as Syn_Ext.XProd (_, _, c, _) =>
45.113 if null (Symtab.lookup_list tab c) then NONE
45.114 else xprod_to_fmt xprod) xprods;
45.115 val tab' = fold (Symtab.remove_list (op =)) fmts tab;
45.116 @@ -290,15 +290,15 @@
45.117 fun token_trans a x =
45.118 (case tokentrf a of
45.119 NONE =>
45.120 - if member (op =) SynExt.standard_token_classes a
45.121 + if member (op =) Syn_Ext.standard_token_classes a
45.122 then SOME (Pretty.str x) else NONE
45.123 | SOME f => SOME (f ctxt x));
45.124
45.125 (*default applications: prefix / postfix*)
45.126 val appT =
45.127 - if type_mode then TypeExt.tappl_ast_tr'
45.128 - else if curried then SynTrans.applC_ast_tr'
45.129 - else SynTrans.appl_ast_tr';
45.130 + if type_mode then Type_Ext.tappl_ast_tr'
45.131 + else if curried then Syn_Trans.applC_ast_tr'
45.132 + else Syn_Trans.appl_ast_tr';
45.133
45.134 fun synT _ ([], args) = ([], args)
45.135 | synT markup (Arg p :: symbs, t :: args) =
45.136 @@ -333,7 +333,7 @@
45.137
45.138 and parT markup (pr, args, p, p': int) = #1 (synT markup
45.139 (if p > p' orelse
45.140 - (! show_brackets andalso p' <> SynExt.max_pri andalso not (is_chain pr))
45.141 + (! show_brackets andalso p' <> Syn_Ext.max_pri andalso not (is_chain pr))
45.142 then [Block (1, Space "(" :: pr @ [Space ")"])]
45.143 else pr, args))
45.144
46.1 --- a/src/Pure/Syntax/syn_ext.ML Mon May 31 19:36:13 2010 +0200
46.2 +++ b/src/Pure/Syntax/syn_ext.ML Mon May 31 21:06:57 2010 +0200
46.3 @@ -41,7 +41,7 @@
46.4 val chain_pri: int
46.5 val delims_of: xprod list -> string list list
46.6 datatype syn_ext =
46.7 - SynExt of {
46.8 + Syn_Ext of {
46.9 xprods: xprod list,
46.10 consts: string list,
46.11 prmodes: string list,
46.12 @@ -86,7 +86,7 @@
46.13 val pure_ext: syn_ext
46.14 end;
46.15
46.16 -structure SynExt: SYN_EXT =
46.17 +structure Syn_Ext: SYN_EXT =
46.18 struct
46.19
46.20
46.21 @@ -326,7 +326,7 @@
46.22 (** datatype syn_ext **)
46.23
46.24 datatype syn_ext =
46.25 - SynExt of {
46.26 + Syn_Ext of {
46.27 xprods: xprod list,
46.28 consts: string list,
46.29 prmodes: string list,
46.30 @@ -352,7 +352,7 @@
46.31 val mfix_consts =
46.32 distinct (op =) (map (fn Mfix x => #3 x) mfixes @ map (fn XProd x => #3 x) xprods);
46.33 in
46.34 - SynExt {
46.35 + Syn_Ext {
46.36 xprods = xprods,
46.37 consts = union (op =) consts mfix_consts,
46.38 prmodes = distinct (op =) (map (fn (m, _, _) => m) tokentrfuns),
47.1 --- a/src/Pure/Syntax/syn_trans.ML Mon May 31 19:36:13 2010 +0200
47.2 +++ b/src/Pure/Syntax/syn_trans.ML Mon May 31 21:06:57 2010 +0200
47.3 @@ -60,7 +60,7 @@
47.4 (string -> (Proof.context -> term list -> term) option) -> Ast.ast list -> term list
47.5 end;
47.6
47.7 -structure SynTrans: SYN_TRANS =
47.8 +structure Syn_Trans: SYN_TRANS =
47.9 struct
47.10
47.11
47.12 @@ -166,7 +166,7 @@
47.13
47.14 (* dddot *)
47.15
47.16 -fun dddot_tr (*"_DDDOT"*) ts = Term.list_comb (Lexicon.var SynExt.dddot_indexname, ts);
47.17 +fun dddot_tr (*"_DDDOT"*) ts = Term.list_comb (Lexicon.var Syn_Ext.dddot_indexname, ts);
47.18
47.19
47.20 (* quote / antiquote *)
47.21 @@ -354,9 +354,9 @@
47.22 (* type propositions *)
47.23
47.24 fun type_prop_tr' _ (*"_type_prop"*) T [Const ("\\<^const>Pure.sort_constraint", _)] =
47.25 - Lexicon.const "_sort_constraint" $ TypeExt.term_of_typ true T
47.26 + Lexicon.const "_sort_constraint" $ Type_Ext.term_of_typ true T
47.27 | type_prop_tr' show_sorts (*"_type_prop"*) T [t] =
47.28 - Lexicon.const "_ofclass" $ TypeExt.term_of_typ show_sorts T $ t
47.29 + Lexicon.const "_ofclass" $ Type_Ext.term_of_typ show_sorts T $ t
47.30 | type_prop_tr' _ (*"_type_prop"*) T ts = raise TYPE ("type_prop_tr'", [T], ts);
47.31
47.32
47.33 @@ -394,7 +394,7 @@
47.34 (* meta implication *)
47.35
47.36 fun impl_ast_tr' (*"==>"*) asts =
47.37 - if TypeExt.no_brackets () then raise Match
47.38 + if Type_Ext.no_brackets () then raise Match
47.39 else
47.40 (case Ast.unfold_ast_p "\\<^const>==>" (Ast.Appl (Ast.Constant "\\<^const>==>" :: asts)) of
47.41 (prems as _ :: _ :: _, concl) =>
47.42 @@ -408,14 +408,14 @@
47.43 (* type reflection *)
47.44
47.45 fun type_tr' show_sorts (*"TYPE"*) (Type ("itself", [T])) ts =
47.46 - Term.list_comb (Lexicon.const "_TYPE" $ TypeExt.term_of_typ show_sorts T, ts)
47.47 + Term.list_comb (Lexicon.const "_TYPE" $ Type_Ext.term_of_typ show_sorts T, ts)
47.48 | type_tr' _ _ _ = raise Match;
47.49
47.50
47.51 (* type constraints *)
47.52
47.53 fun type_constraint_tr' show_sorts (*"_type_constraint_"*) (Type ("fun", [T, _])) (t :: ts) =
47.54 - Term.list_comb (Lexicon.const SynExt.constrainC $ t $ TypeExt.term_of_typ show_sorts T, ts)
47.55 + Term.list_comb (Lexicon.const Syn_Ext.constrainC $ t $ Type_Ext.term_of_typ show_sorts T, ts)
47.56 | type_constraint_tr' _ _ _ = raise Match;
47.57
47.58
48.1 --- a/src/Pure/Syntax/syntax.ML Mon May 31 19:36:13 2010 +0200
48.2 +++ b/src/Pure/Syntax/syntax.ML Mon May 31 21:06:57 2010 +0200
48.3 @@ -168,21 +168,21 @@
48.4 fun err_dup_trfun name c =
48.5 error ("More than one " ^ name ^ " for " ^ quote c);
48.6
48.7 -fun remove_trtab trfuns = fold (Symtab.remove SynExt.eq_trfun) trfuns;
48.8 +fun remove_trtab trfuns = fold (Symtab.remove Syn_Ext.eq_trfun) trfuns;
48.9
48.10 fun update_trtab name trfuns tab = fold Symtab.update_new trfuns (remove_trtab trfuns tab)
48.11 handle Symtab.DUP c => err_dup_trfun name c;
48.12
48.13 -fun merge_trtabs name tab1 tab2 = Symtab.merge SynExt.eq_trfun (tab1, tab2)
48.14 +fun merge_trtabs name tab1 tab2 = Symtab.merge Syn_Ext.eq_trfun (tab1, tab2)
48.15 handle Symtab.DUP c => err_dup_trfun name c;
48.16
48.17
48.18 (* print (ast) translations *)
48.19
48.20 fun lookup_tr' tab c = map fst (Symtab.lookup_list tab c);
48.21 -fun update_tr'tab trfuns = fold_rev (Symtab.update_list SynExt.eq_trfun) trfuns;
48.22 -fun remove_tr'tab trfuns = fold (Symtab.remove_list SynExt.eq_trfun) trfuns;
48.23 -fun merge_tr'tabs tab1 tab2 = Symtab.merge_list SynExt.eq_trfun (tab1, tab2);
48.24 +fun update_tr'tab trfuns = fold_rev (Symtab.update_list Syn_Ext.eq_trfun) trfuns;
48.25 +fun remove_tr'tab trfuns = fold (Symtab.remove_list Syn_Ext.eq_trfun) trfuns;
48.26 +fun merge_tr'tabs tab1 tab2 = Symtab.merge_list Syn_Ext.eq_trfun (tab1, tab2);
48.27
48.28
48.29
48.30 @@ -239,7 +239,7 @@
48.31
48.32 datatype syntax =
48.33 Syntax of {
48.34 - input: SynExt.xprod list,
48.35 + input: Syn_Ext.xprod list,
48.36 lexicon: Scan.lexicon,
48.37 gram: Parser.gram,
48.38 consts: string list,
48.39 @@ -287,7 +287,7 @@
48.40 val {input, lexicon, gram, consts = consts1, prmodes = prmodes1,
48.41 parse_ast_trtab, parse_ruletab, parse_trtab, print_trtab, print_ruletab,
48.42 print_ast_trtab, tokentrtab, prtabs} = tabs;
48.43 - val SynExt.SynExt {xprods, consts = consts2, prmodes = prmodes2,
48.44 + val Syn_Ext.Syn_Ext {xprods, consts = consts2, prmodes = prmodes2,
48.45 parse_ast_translation, parse_rules, parse_translation, print_translation, print_rules,
48.46 print_ast_translation, token_translation} = syn_ext;
48.47 val new_xprods =
48.48 @@ -296,7 +296,7 @@
48.49 in
48.50 Syntax
48.51 ({input = new_xprods @ input,
48.52 - lexicon = fold Scan.extend_lexicon (SynExt.delims_of new_xprods) lexicon,
48.53 + lexicon = fold Scan.extend_lexicon (Syn_Ext.delims_of new_xprods) lexicon,
48.54 gram = Parser.extend_gram gram new_xprods,
48.55 consts = Library.merge (op =) (consts1, filter_out Lexicon.is_marked consts2),
48.56 prmodes = insert (op =) mode (Library.merge (op =) (prmodes1, prmodes2)),
48.57 @@ -316,7 +316,7 @@
48.58
48.59 fun remove_syntax (mode, inout) syn_ext (Syntax (tabs, _)) =
48.60 let
48.61 - val SynExt.SynExt {xprods, consts = _, prmodes = _,
48.62 + val Syn_Ext.Syn_Ext {xprods, consts = _, prmodes = _,
48.63 parse_ast_translation, parse_rules, parse_translation, print_translation, print_rules,
48.64 print_ast_translation, token_translation = _} = syn_ext;
48.65 val {input, lexicon, gram, consts, prmodes,
48.66 @@ -328,7 +328,7 @@
48.67 in
48.68 Syntax
48.69 ({input = input',
48.70 - lexicon = if changed then Scan.make_lexicon (SynExt.delims_of input') else lexicon,
48.71 + lexicon = if changed then Scan.make_lexicon (Syn_Ext.delims_of input') else lexicon,
48.72 gram = if changed then Parser.make_gram input' else gram,
48.73 consts = consts,
48.74 prmodes = prmodes,
48.75 @@ -381,13 +381,13 @@
48.76
48.77 val basic_syntax =
48.78 empty_syntax
48.79 - |> update_syntax mode_default TypeExt.type_ext
48.80 - |> update_syntax mode_default SynExt.pure_ext;
48.81 + |> update_syntax mode_default Type_Ext.type_ext
48.82 + |> update_syntax mode_default Syn_Ext.pure_ext;
48.83
48.84 val basic_nonterms =
48.85 - (Lexicon.terminals @ [SynExt.logic, "type", "types", "sort", "classes",
48.86 - SynExt.args, SynExt.cargs, "pttrn", "pttrns", "idt", "idts", "aprop",
48.87 - "asms", SynExt.any, SynExt.sprop, "num_const", "float_const",
48.88 + (Lexicon.terminals @ [Syn_Ext.logic, "type", "types", "sort", "classes",
48.89 + Syn_Ext.args, Syn_Ext.cargs, "pttrn", "pttrns", "idt", "idts", "aprop",
48.90 + "asms", Syn_Ext.any, Syn_Ext.sprop, "num_const", "float_const",
48.91 "index", "struct"]);
48.92
48.93
48.94 @@ -481,13 +481,13 @@
48.95 val toks = Lexicon.tokenize lexicon xids syms;
48.96 val _ = List.app Lexicon.report_token toks;
48.97
48.98 - val root' = if root <> "prop" andalso is_logtype root then SynExt.logic else root;
48.99 + val root' = if root <> "prop" andalso is_logtype root then Syn_Ext.logic else root;
48.100 val pts = Parser.parse gram root' (filter Lexicon.is_proper toks);
48.101 val len = length pts;
48.102
48.103 val limit = ! ambiguity_limit;
48.104 fun show_pt pt =
48.105 - Pretty.string_of (Ast.pretty_ast (hd (SynTrans.pts_to_asts ctxt (K NONE) [pt])));
48.106 + Pretty.string_of (Ast.pretty_ast (hd (Syn_Trans.pts_to_asts ctxt (K NONE) [pt])));
48.107 in
48.108 if len <= ! ambiguity_level then ()
48.109 else if ! ambiguity_is_error then error (ambiguity_msg pos)
48.110 @@ -497,7 +497,7 @@
48.111 "\nproduces " ^ string_of_int len ^ " parse trees" ^
48.112 (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
48.113 map show_pt (take limit pts))));
48.114 - SynTrans.pts_to_asts ctxt (lookup_tr parse_ast_trtab) pts
48.115 + Syn_Trans.pts_to_asts ctxt (lookup_tr parse_ast_trtab) pts
48.116 end;
48.117
48.118
48.119 @@ -506,9 +506,9 @@
48.120 fun read ctxt is_logtype (syn as Syntax (tabs, _)) ty inp =
48.121 let
48.122 val {parse_ruletab, parse_trtab, ...} = tabs;
48.123 - val asts = read_asts ctxt is_logtype syn false (SynExt.typ_to_nonterm ty) inp;
48.124 + val asts = read_asts ctxt is_logtype syn false (Syn_Ext.typ_to_nonterm ty) inp;
48.125 in
48.126 - SynTrans.asts_to_terms ctxt (lookup_tr parse_trtab)
48.127 + Syn_Trans.asts_to_terms ctxt (lookup_tr parse_trtab)
48.128 (map (Ast.normalize_ast (Symtab.lookup_list parse_ruletab)) asts)
48.129 end;
48.130
48.131 @@ -547,23 +547,23 @@
48.132
48.133 fun standard_parse_term pp check get_sort map_const map_free ctxt is_logtype syn ty (syms, pos) =
48.134 read ctxt is_logtype syn ty (syms, pos)
48.135 - |> map (TypeExt.decode_term get_sort map_const map_free)
48.136 + |> map (Type_Ext.decode_term get_sort map_const map_free)
48.137 |> disambig (Printer.pp_show_brackets pp) check;
48.138
48.139
48.140 (* read types *)
48.141
48.142 fun standard_parse_typ ctxt syn get_sort (syms, pos) =
48.143 - (case read ctxt (K false) syn SynExt.typeT (syms, pos) of
48.144 - [t] => TypeExt.typ_of_term (get_sort (TypeExt.term_sorts t)) t
48.145 + (case read ctxt (K false) syn Syn_Ext.typeT (syms, pos) of
48.146 + [t] => Type_Ext.typ_of_term (get_sort (Type_Ext.term_sorts t)) t
48.147 | _ => error (ambiguity_msg pos));
48.148
48.149
48.150 (* read sorts *)
48.151
48.152 fun standard_parse_sort ctxt syn (syms, pos) =
48.153 - (case read ctxt (K false) syn TypeExt.sortT (syms, pos) of
48.154 - [t] => TypeExt.sort_of_term t
48.155 + (case read ctxt (K false) syn Type_Ext.sortT (syms, pos) of
48.156 + [t] => Type_Ext.sort_of_term t
48.157 | _ => error (ambiguity_msg pos));
48.158
48.159
48.160 @@ -666,9 +666,9 @@
48.161
48.162 fun ext_syntax f decls = update_syntax mode_default (f decls);
48.163
48.164 -val update_trfuns = ext_syntax SynExt.syn_ext_trfuns;
48.165 -val update_advanced_trfuns = ext_syntax SynExt.syn_ext_advanced_trfuns;
48.166 -val extend_tokentrfuns = ext_syntax SynExt.syn_ext_tokentrfuns;
48.167 +val update_trfuns = ext_syntax Syn_Ext.syn_ext_trfuns;
48.168 +val update_advanced_trfuns = ext_syntax Syn_Ext.syn_ext_advanced_trfuns;
48.169 +val extend_tokentrfuns = ext_syntax Syn_Ext.syn_ext_tokentrfuns;
48.170
48.171 fun update_type_gram add prmode decls =
48.172 (if add then update_syntax else remove_syntax) prmode (Mixfix.syn_ext_types decls);
48.173 @@ -677,13 +677,13 @@
48.174 (if add then update_syntax else remove_syntax) prmode (Mixfix.syn_ext_consts is_logtype decls);
48.175
48.176 fun update_trrules ctxt is_logtype syn =
48.177 - ext_syntax SynExt.syn_ext_rules o read_rules ctxt is_logtype syn;
48.178 + ext_syntax Syn_Ext.syn_ext_rules o read_rules ctxt is_logtype syn;
48.179
48.180 fun remove_trrules ctxt is_logtype syn =
48.181 - remove_syntax mode_default o SynExt.syn_ext_rules o read_rules ctxt is_logtype syn;
48.182 + remove_syntax mode_default o Syn_Ext.syn_ext_rules o read_rules ctxt is_logtype syn;
48.183
48.184 -val update_trrules_i = ext_syntax SynExt.syn_ext_rules o cert_rules;
48.185 -val remove_trrules_i = remove_syntax mode_default o SynExt.syn_ext_rules o cert_rules;
48.186 +val update_trrules_i = ext_syntax Syn_Ext.syn_ext_rules o cert_rules;
48.187 +val remove_trrules_i = remove_syntax mode_default o Syn_Ext.syn_ext_rules o cert_rules;
48.188
48.189
48.190
48.191 @@ -798,7 +798,7 @@
48.192
48.193 val check_typs = gen_check fst false;
48.194 val check_terms = gen_check snd false;
48.195 -fun check_props ctxt = map (TypeExt.type_constraint propT) #> check_terms ctxt;
48.196 +fun check_props ctxt = map (Type_Ext.type_constraint propT) #> check_terms ctxt;
48.197
48.198 val check_typ = singleton o check_typs;
48.199 val check_term = singleton o check_terms;
48.200 @@ -905,7 +905,7 @@
48.201
48.202
48.203 (*export parts of internal Syntax structures*)
48.204 -open Lexicon SynExt Ast Parser TypeExt SynTrans Mixfix Printer;
48.205 +open Lexicon Syn_Ext Ast Parser Type_Ext Syn_Trans Mixfix Printer;
48.206
48.207 end;
48.208
48.209 @@ -913,9 +913,9 @@
48.210 open Basic_Syntax;
48.211
48.212 forget_structure "Ast";
48.213 -forget_structure "SynExt";
48.214 +forget_structure "Syn_Ext";
48.215 forget_structure "Parser";
48.216 -forget_structure "TypeExt";
48.217 -forget_structure "SynTrans";
48.218 +forget_structure "Type_Ext";
48.219 +forget_structure "Syn_Trans";
48.220 forget_structure "Mixfix";
48.221 forget_structure "Printer";
49.1 --- a/src/Pure/Syntax/type_ext.ML Mon May 31 19:36:13 2010 +0200
49.2 +++ b/src/Pure/Syntax/type_ext.ML Mon May 31 21:06:57 2010 +0200
49.3 @@ -27,10 +27,10 @@
49.4 val term_of_sort: sort -> term
49.5 val tappl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
49.6 val sortT: typ
49.7 - val type_ext: SynExt.syn_ext
49.8 + val type_ext: Syn_Ext.syn_ext
49.9 end;
49.10
49.11 -structure TypeExt: TYPE_EXT =
49.12 +structure Type_Ext: TYPE_EXT =
49.13 struct
49.14
49.15 (** input utils **)
49.16 @@ -242,7 +242,7 @@
49.17 val classesT = Type ("classes", []);
49.18 val typesT = Type ("types", []);
49.19
49.20 -local open Lexicon SynExt in
49.21 +local open Lexicon Syn_Ext in
49.22
49.23 val type_ext = syn_ext' false (K false)
49.24 [Mfix ("_", tidT --> typeT, "", [], max_pri),
49.25 @@ -271,7 +271,7 @@
49.26 Mfix ("'(_')", typeT --> typeT, "", [0], max_pri),
49.27 Mfix ("'_", typeT, "\\<^type>dummy", [], max_pri)]
49.28 ["_type_prop"]
49.29 - ([], [], [], map SynExt.mk_trfun [("\\<^type>fun", K fun_ast_tr')])
49.30 + ([], [], [], map Syn_Ext.mk_trfun [("\\<^type>fun", K fun_ast_tr')])
49.31 []
49.32 ([], []);
49.33
50.1 --- a/src/Pure/System/isabelle_process.ML Mon May 31 19:36:13 2010 +0200
50.2 +++ b/src/Pure/System/isabelle_process.ML Mon May 31 21:06:57 2010 +0200
50.3 @@ -67,9 +67,9 @@
50.4 val path = File.platform_path (Path.explode out);
50.5 val out_stream = TextIO.openOut path; (*fifo blocks until reader is ready*)
50.6 val _ = OS.FileSys.remove path; (*prevent alien access, indicate writer is ready*)
50.7 - val _ = SimpleThread.fork false (auto_flush out_stream);
50.8 - val _ = SimpleThread.fork false (auto_flush TextIO.stdOut);
50.9 - val _ = SimpleThread.fork false (auto_flush TextIO.stdErr);
50.10 + val _ = Simple_Thread.fork false (auto_flush out_stream);
50.11 + val _ = Simple_Thread.fork false (auto_flush TextIO.stdOut);
50.12 + val _ = Simple_Thread.fork false (auto_flush TextIO.stdErr);
50.13 in
50.14 Output.status_fn := standard_message out_stream "B";
50.15 Output.writeln_fn := standard_message out_stream "C";
51.1 --- a/src/Pure/System/isar.ML Mon May 31 19:36:13 2010 +0200
51.2 +++ b/src/Pure/System/isar.ML Mon May 31 21:06:57 2010 +0200
51.3 @@ -72,7 +72,7 @@
51.4
51.5 fun find_and_undo _ [] = error "Undo history exhausted"
51.6 | find_and_undo which ((prev, tr) :: hist) =
51.7 - ((case Toplevel.init_of tr of SOME name => ThyInfo.kill_thy name | NONE => ());
51.8 + ((case Toplevel.init_of tr of SOME name => Thy_Info.kill_thy name | NONE => ());
51.9 if which (Toplevel.name_of tr) then (prev, hist) else find_and_undo which hist);
51.10
51.11 in
52.1 --- a/src/Pure/System/session.ML Mon May 31 19:36:13 2010 +0200
52.2 +++ b/src/Pure/System/session.ML Mon May 31 21:06:57 2010 +0200
52.3 @@ -73,7 +73,7 @@
52.4 (* finish *)
52.5
52.6 fun finish () =
52.7 - (ThyInfo.finish ();
52.8 + (Thy_Info.finish ();
52.9 Present.finish ();
52.10 Future.shutdown ();
52.11 session_finished := true);
52.12 @@ -97,7 +97,7 @@
52.13 ((fn () =>
52.14 (init reset parent name;
52.15 Present.init build info doc doc_graph doc_versions (path ()) name
52.16 - (dumping dump) (get_rpath rpath) verbose (map ThyInfo.get_theory (ThyInfo.get_names ()));
52.17 + (dumping dump) (get_rpath rpath) verbose (map Thy_Info.get_theory (Thy_Info.get_names ()));
52.18 if timing then
52.19 let
52.20 val start = start_timing ();
53.1 --- a/src/Pure/Thy/present.ML Mon May 31 19:36:13 2010 +0200
53.2 +++ b/src/Pure/Thy/present.ML Mon May 31 21:06:57 2010 +0200
53.3 @@ -461,7 +461,7 @@
53.4 val parent_specs = map (parent_link remote_path path) parents;
53.5
53.6 fun prep_file (raw_path, loadit) =
53.7 - (case ThyLoad.check_ml dir raw_path of
53.8 + (case Thy_Load.check_ml dir raw_path of
53.9 SOME (path, _) =>
53.10 let
53.11 val base = Path.base path;
54.1 --- a/src/Pure/Thy/thm_deps.ML Mon May 31 19:36:13 2010 +0200
54.2 +++ b/src/Pure/Thy/thm_deps.ML Mon May 31 21:06:57 2010 +0200
54.3 @@ -24,7 +24,7 @@
54.4 val session =
54.5 (case prefix of
54.6 a :: _ =>
54.7 - (case ThyInfo.lookup_theory a of
54.8 + (case Thy_Info.lookup_theory a of
54.9 SOME thy =>
54.10 (case Present.session_name thy of
54.11 "" => []
55.1 --- a/src/Pure/Thy/thy_info.ML Mon May 31 19:36:13 2010 +0200
55.2 +++ b/src/Pure/Thy/thy_info.ML Mon May 31 21:06:57 2010 +0200
55.3 @@ -41,7 +41,7 @@
55.4 val finish: unit -> unit
55.5 end;
55.6
55.7 -structure ThyInfo: THY_INFO =
55.8 +structure Thy_Info: THY_INFO =
55.9 struct
55.10
55.11 (** theory loader actions and hooks **)
55.12 @@ -292,12 +292,12 @@
55.13
55.14 fun run_file path =
55.15 (case Option.map (Context.theory_name o Context.the_theory) (Context.thread_data ()) of
55.16 - NONE => (ThyLoad.load_ml Path.current path; ())
55.17 + NONE => (Thy_Load.load_ml Path.current path; ())
55.18 | SOME name =>
55.19 (case lookup_deps name of
55.20 SOME deps =>
55.21 - change_deps name (provide path name (ThyLoad.load_ml (master_dir' deps) path))
55.22 - | NONE => (ThyLoad.load_ml Path.current path; ())));
55.23 + change_deps name (provide path name (Thy_Load.load_ml (master_dir' deps) path))
55.24 + | NONE => (Thy_Load.load_ml Path.current path; ())));
55.25
55.26 in
55.27
55.28 @@ -306,7 +306,7 @@
55.29 val dir = master_directory name;
55.30 val _ = check_unfinished error name;
55.31 in
55.32 - (case ThyLoad.check_file dir path of
55.33 + (case Thy_Load.check_file dir path of
55.34 SOME path_info => change_deps name (provide path name path_info)
55.35 | NONE => error ("Could not find file " ^ quote (Path.implode path)))
55.36 end;
55.37 @@ -429,7 +429,7 @@
55.38 let val info' =
55.39 (case info of NONE => NONE
55.40 | SOME (_, id) =>
55.41 - (case ThyLoad.check_ml (master_dir master) src_path of NONE => NONE
55.42 + (case Thy_Load.check_ml (master_dir master) src_path of NONE => NONE
55.43 | SOME (path', id') => if id <> id' then NONE else SOME (path', id')))
55.44 in (src_path, info') end;
55.45
55.46 @@ -437,16 +437,16 @@
55.47 (case lookup_deps name of
55.48 SOME NONE => (true, NONE, get_parents name)
55.49 | NONE =>
55.50 - let val {master, text, imports = parents, uses = files} = ThyLoad.deps_thy dir name
55.51 + let val {master, text, imports = parents, uses = files} = Thy_Load.deps_thy dir name
55.52 in (false, init_deps (SOME master) text parents files, parents) end
55.53 | SOME (SOME {update_time, master, text, parents, files}) =>
55.54 let
55.55 - val (thy_path, thy_id) = ThyLoad.check_thy dir name;
55.56 + val (thy_path, thy_id) = Thy_Load.check_thy dir name;
55.57 val master' = SOME (thy_path, thy_id);
55.58 in
55.59 if Option.map #2 master <> SOME thy_id then
55.60 let val {text = text', imports = parents', uses = files', ...} =
55.61 - ThyLoad.deps_thy dir name;
55.62 + Thy_Load.deps_thy dir name;
55.63 in (false, init_deps master' text' parents' files', parents') end
55.64 else
55.65 let
55.66 @@ -571,7 +571,7 @@
55.67 val _ = map get_theory (get_parents name);
55.68 val _ = check_unfinished error name;
55.69 val _ = touch_thy name;
55.70 - val master = #master (ThyLoad.deps_thy Path.current name);
55.71 + val master = #master (Thy_Load.deps_thy Path.current name);
55.72 val upd_time = #2 (Management_Data.get thy);
55.73 in
55.74 CRITICAL (fn () =>
56.1 --- a/src/Pure/Thy/thy_load.ML Mon May 31 19:36:13 2010 +0200
56.2 +++ b/src/Pure/Thy/thy_load.ML Mon May 31 21:06:57 2010 +0200
56.3 @@ -31,10 +31,9 @@
56.4 val load_ml: Path.T -> Path.T -> Path.T * File.ident
56.5 end;
56.6
56.7 -structure ThyLoad: THY_LOAD =
56.8 +structure Thy_Load: THY_LOAD =
56.9 struct
56.10
56.11 -
56.12 (* maintain load path *)
56.13
56.14 local val load_path = Unsynchronized.ref [Path.current] in
56.15 @@ -132,5 +131,5 @@
56.16
56.17 end;
56.18
56.19 -structure Basic_Thy_Load: BASIC_THY_LOAD = ThyLoad;
56.20 +structure Basic_Thy_Load: BASIC_THY_LOAD = Thy_Load;
56.21 open Basic_Thy_Load;
57.1 --- a/src/Pure/Thy/thy_output.ML Mon May 31 19:36:13 2010 +0200
57.2 +++ b/src/Pure/Thy/thy_output.ML Mon May 31 21:06:57 2010 +0200
57.3 @@ -33,7 +33,7 @@
57.4 val output: Pretty.T list -> string
57.5 end;
57.6
57.7 -structure ThyOutput: THY_OUTPUT =
57.8 +structure Thy_Output: THY_OUTPUT =
57.9 struct
57.10
57.11 (** global options **)
58.1 --- a/src/Pure/Thy/thy_syntax.ML Mon May 31 19:36:13 2010 +0200
58.2 +++ b/src/Pure/Thy/thy_syntax.ML Mon May 31 21:06:57 2010 +0200
58.3 @@ -25,7 +25,7 @@
58.4 (span * span list * bool, (span, 'a) Source.source) Source.source
58.5 end;
58.6
58.7 -structure ThySyntax: THY_SYNTAX =
58.8 +structure Thy_Syntax: THY_SYNTAX =
58.9 struct
58.10
58.11 (** tokens **)
59.1 --- a/src/Pure/context.ML Mon May 31 19:36:13 2010 +0200
59.2 +++ b/src/Pure/context.ML Mon May 31 21:06:57 2010 +0200
59.3 @@ -325,7 +325,7 @@
59.4 local
59.5 val lock = Mutex.mutex ();
59.6 in
59.7 - fun SYNCHRONIZED e = SimpleThread.synchronized "theory" lock e;
59.8 + fun SYNCHRONIZED e = Simple_Thread.synchronized "theory" lock e;
59.9 end;
59.10
59.11 fun create_thy self draft ids data ancestry history =
60.1 --- a/src/Pure/morphism.ML Mon May 31 19:36:13 2010 +0200
60.2 +++ b/src/Pure/morphism.ML Mon May 31 21:06:57 2010 +0200
60.3 @@ -79,5 +79,5 @@
60.4
60.5 end;
60.6
60.7 -structure BasicMorphism: BASIC_MORPHISM = Morphism;
60.8 -open BasicMorphism;
60.9 +structure Basic_Morphism: BASIC_MORPHISM = Morphism;
60.10 +open Basic_Morphism;
61.1 --- a/src/Pure/proofterm.ML Mon May 31 19:36:13 2010 +0200
61.2 +++ b/src/Pure/proofterm.ML Mon May 31 21:06:57 2010 +0200
61.3 @@ -1328,7 +1328,7 @@
61.4
61.5 (**** theory data ****)
61.6
61.7 -structure ProofData = Theory_Data
61.8 +structure Data = Theory_Data
61.9 (
61.10 type T =
61.11 (stamp * (proof * proof)) list *
61.12 @@ -1341,11 +1341,11 @@
61.13 AList.merge (op =) (K true) (procs1, procs2));
61.14 );
61.15
61.16 -fun get_data thy = let val (rules, procs) = ProofData.get thy in (map #2 rules, map #2 procs) end;
61.17 +fun get_data thy = let val (rules, procs) = Data.get thy in (map #2 rules, map #2 procs) end;
61.18 fun rew_proof thy = rewrite_prf fst (get_data thy);
61.19
61.20 -fun add_prf_rrule r = (ProofData.map o apfst) (cons (stamp (), r));
61.21 -fun add_prf_rproc p = (ProofData.map o apsnd) (cons (stamp (), p));
61.22 +fun add_prf_rrule r = (Data.map o apfst) (cons (stamp (), r));
61.23 +fun add_prf_rproc p = (Data.map o apsnd) (cons (stamp (), p));
61.24
61.25
61.26 (***** promises *****)
62.1 --- a/src/Pure/pure_setup.ML Mon May 31 19:36:13 2010 +0200
62.2 +++ b/src/Pure/pure_setup.ML Mon May 31 21:06:57 2010 +0200
62.3 @@ -6,14 +6,14 @@
62.4
62.5 (* the Pure theories *)
62.6
62.7 -val theory = ThyInfo.get_theory;
62.8 +val theory = Thy_Info.get_theory;
62.9
62.10 Context.>> (Context.map_theory
62.11 (Outer_Syntax.process_file (Path.explode "Pure.thy") #>
62.12 Theory.end_theory));
62.13 structure Pure = struct val thy = ML_Context.the_global_context () end;
62.14 Context.set_thread_data NONE;
62.15 -ThyInfo.register_theory Pure.thy;
62.16 +Thy_Info.register_theory Pure.thy;
62.17
62.18
62.19 (* ML toplevel pretty printing *)
62.20 @@ -47,11 +47,11 @@
62.21
62.22 (* ML toplevel use commands *)
62.23
62.24 -fun use name = Toplevel.program (fn () => ThyInfo.use name);
62.25 -fun use_thys name = Toplevel.program (fn () => ThyInfo.use_thys name);
62.26 -fun use_thy name = Toplevel.program (fn () => ThyInfo.use_thy name);
62.27 -fun time_use name = Toplevel.program (fn () => ThyInfo.time_use name);
62.28 -fun time_use_thy name = Toplevel.program (fn () => ThyInfo.time_use_thy name);
62.29 +fun use name = Toplevel.program (fn () => Thy_Info.use name);
62.30 +fun use_thys name = Toplevel.program (fn () => Thy_Info.use_thys name);
62.31 +fun use_thy name = Toplevel.program (fn () => Thy_Info.use_thy name);
62.32 +fun time_use name = Toplevel.program (fn () => Thy_Info.time_use name);
62.33 +fun time_use_thy name = Toplevel.program (fn () => Thy_Info.time_use_thy name);
62.34
62.35
62.36 (* misc *)
63.1 --- a/src/Pure/pure_thy.ML Mon May 31 19:36:13 2010 +0200
63.2 +++ b/src/Pure/pure_thy.ML Mon May 31 21:06:57 2010 +0200
63.3 @@ -52,7 +52,7 @@
63.4
63.5 (** theory data **)
63.6
63.7 -structure FactsData = Theory_Data
63.8 +structure Global_Facts = Theory_Data
63.9 (
63.10 type T = Facts.T * thm list;
63.11 val empty = (Facts.empty, []);
63.12 @@ -63,19 +63,19 @@
63.13
63.14 (* facts *)
63.15
63.16 -val facts_of = #1 o FactsData.get;
63.17 +val facts_of = #1 o Global_Facts.get;
63.18
63.19 val intern_fact = Facts.intern o facts_of;
63.20 val defined_fact = Facts.defined o facts_of;
63.21
63.22 -fun hide_fact fully name = FactsData.map (apfst (Facts.hide fully name));
63.23 +fun hide_fact fully name = Global_Facts.map (apfst (Facts.hide fully name));
63.24
63.25
63.26 (* proofs *)
63.27
63.28 -fun register_proofs (thy, thms) = (FactsData.map (apsnd (append thms)) thy, thms);
63.29 +fun register_proofs (thy, thms) = (Global_Facts.map (apsnd (append thms)) thy, thms);
63.30
63.31 -fun join_proofs thy = Thm.join_proofs (rev (#2 (FactsData.get thy)));
63.32 +fun join_proofs thy = Thm.join_proofs (rev (#2 (Global_Facts.get thy)));
63.33
63.34
63.35
63.36 @@ -143,7 +143,7 @@
63.37 val (thy', thms') =
63.38 register_proofs (apsnd (post_name name) (app_att (thy, pre_name name thms)));
63.39 val thms'' = map (Thm.transfer thy') thms';
63.40 - val thy'' = thy' |> (FactsData.map o apfst) (Facts.add_global naming (b, thms'') #> snd);
63.41 + val thy'' = thy' |> (Global_Facts.map o apfst) (Facts.add_global naming (b, thms'') #> snd);
63.42 in (thms'', thy'') end;
63.43
63.44
63.45 @@ -178,7 +178,7 @@
63.46 (* add_thms_dynamic *)
63.47
63.48 fun add_thms_dynamic (b, f) thy = thy
63.49 - |> (FactsData.map o apfst)
63.50 + |> (Global_Facts.map o apfst)
63.51 (Facts.add_dynamic (Sign.naming_of thy) (b, f) #> snd);
63.52
63.53
63.54 @@ -252,7 +252,7 @@
63.55 ("_applC", typ "('b => 'a) => cargs => logic", Mixfix ("(1_/ _)", [1000, 1000], 999)),
63.56 ("_applC", typ "('b => 'a) => cargs => aprop", Mixfix ("(1_/ _)", [1000, 1000], 999))];
63.57
63.58 -structure OldApplSyntax = Theory_Data
63.59 +structure Old_Appl_Syntax = Theory_Data
63.60 (
63.61 type T = bool;
63.62 val empty = false;
63.63 @@ -262,10 +262,10 @@
63.64 else error "Cannot merge theories with different application syntax";
63.65 );
63.66
63.67 -val old_appl_syntax = OldApplSyntax.get;
63.68 +val old_appl_syntax = Old_Appl_Syntax.get;
63.69
63.70 val old_appl_syntax_setup =
63.71 - OldApplSyntax.put true #>
63.72 + Old_Appl_Syntax.put true #>
63.73 Sign.del_modesyntax_i Syntax.mode_default applC_syntax #>
63.74 Sign.add_syntax_i appl_syntax;
63.75
63.76 @@ -274,7 +274,7 @@
63.77
63.78 val _ = Context.>> (Context.map_theory
63.79 (Sign.map_naming (Name_Space.set_theory_name Context.PureN) #>
63.80 - OldApplSyntax.put false #>
63.81 + Old_Appl_Syntax.put false #>
63.82 Sign.add_types
63.83 [(Binding.name "fun", 2, NoSyn),
63.84 (Binding.name "prop", 0, NoSyn),
64.1 --- a/src/Pure/simplifier.ML Mon May 31 19:36:13 2010 +0200
64.2 +++ b/src/Pure/simplifier.ML Mon May 31 21:06:57 2010 +0200
64.3 @@ -100,7 +100,7 @@
64.4
64.5 (** simpset data **)
64.6
64.7 -structure SimpsetData = Generic_Data
64.8 +structure Simpset = Generic_Data
64.9 (
64.10 type T = simpset;
64.11 val empty = empty_ss;
64.12 @@ -108,8 +108,8 @@
64.13 val merge = merge_ss;
64.14 );
64.15
64.16 -val get_ss = SimpsetData.get;
64.17 -fun map_ss f context = SimpsetData.map (with_context (Context.proof_of context) f) context;
64.18 +val get_ss = Simpset.get;
64.19 +fun map_ss f context = Simpset.map (with_context (Context.proof_of context) f) context;
64.20
64.21
64.22 (* attributes *)
65.1 --- a/src/Tools/Code/code_eval.ML Mon May 31 19:36:13 2010 +0200
65.2 +++ b/src/Tools/Code/code_eval.ML Mon May 31 21:06:57 2010 +0200
65.3 @@ -173,7 +173,7 @@
65.4 end
65.5 | process (code_body, _) _ (SOME file_name) thy =
65.6 let
65.7 - val preamble = "(* Generated from " ^ Path.implode (ThyLoad.thy_path (Context.theory_name thy))
65.8 + val preamble = "(* Generated from " ^ Path.implode (Thy_Load.thy_path (Context.theory_name thy))
65.9 ^ "; DO NOT EDIT! *)";
65.10 val _ = File.write (Path.explode file_name) (preamble ^ "\n\n" ^ code_body);
65.11 in
66.1 --- a/src/Tools/Code/code_thingol.ML Mon May 31 19:36:13 2010 +0200
66.2 +++ b/src/Tools/Code/code_thingol.ML Mon May 31 21:06:57 2010 +0200
66.3 @@ -882,7 +882,7 @@
66.4 fun consts_of_select thy' = filter (belongs_here thy') (consts_of thy');
66.5 fun read_const_expr "*" = ([], consts_of thy)
66.6 | read_const_expr s = if String.isSuffix ".*" s
66.7 - then ([], consts_of_select (ThyInfo.the_theory (unsuffix ".*" s) thy))
66.8 + then ([], consts_of_select (Thy_Info.the_theory (unsuffix ".*" s) thy))
66.9 else ([Code.read_const thy s], []);
66.10 in pairself flat o split_list o map read_const_expr end;
66.11
67.1 --- a/src/Tools/WWW_Find/find_theorems.ML Mon May 31 19:36:13 2010 +0200
67.2 +++ b/src/Tools/WWW_Find/find_theorems.ML Mon May 31 21:06:57 2010 +0200
67.3 @@ -5,8 +5,9 @@
67.4 *)
67.5
67.6 local
67.7 +
67.8 val default_limit = 20;
67.9 -val thy_names = sort string_ord (ThyInfo.get_names ());
67.10 +val thy_names = sort string_ord (Thy_Info.get_names ());
67.11
67.12 val find_theorems_url = "find_theorems";
67.13
67.14 @@ -234,7 +235,9 @@
67.15 Xhtml.write_close send header
67.16 end;
67.17 in
67.18 +
67.19 val () = show_question_marks := false;
67.20 val () = ScgiServer.register (find_theorems_url, SOME Mime.html, find_theorems);
67.21 +
67.22 end;
67.23