# HG changeset patch # User wenzelm # Date 1529585361 -7200 # Node ID cb84beb84ca962e8a2a36579e38a82e8124610a4 # Parent fb6afa538b04eb46e82f54e2f586639efa05fbc1 clarified signature; diff -r fb6afa538b04 -r cb84beb84ca9 src/Pure/ML/ml_antiquotations.ML --- a/src/Pure/ML/ml_antiquotations.ML Thu Jun 21 14:29:44 2018 +0200 +++ b/src/Pure/ML/ml_antiquotations.ML Thu Jun 21 14:49:21 2018 +0200 @@ -46,13 +46,14 @@ ML_Antiquotation.value \<^binding>\theory\ (Args.context -- Scan.lift (Parse.position Args.embedded) >> (fn (ctxt, (name, pos)) => - (Theory.check ctxt (name, pos); - "Context.get_theory (Proof_Context.theory_of ML_context) " ^ ML_Syntax.print_string name)) + (Theory.check {long = false} ctxt (name, pos); + "Context.get_theory {long = false} (Proof_Context.theory_of ML_context) " ^ + ML_Syntax.print_string name)) || Scan.succeed "Proof_Context.theory_of ML_context") #> ML_Antiquotation.value \<^binding>\theory_context\ (Args.context -- Scan.lift (Parse.position Args.embedded) >> (fn (ctxt, (name, pos)) => - (Theory.check ctxt (name, pos); + (Theory.check {long = false} ctxt (name, pos); "Proof_Context.get_global (Proof_Context.theory_of ML_context) " ^ ML_Syntax.print_string name))) #> diff -r fb6afa538b04 -r cb84beb84ca9 src/Pure/Pure.thy --- a/src/Pure/Pure.thy Thu Jun 21 14:29:44 2018 +0200 +++ b/src/Pure/Pure.thy Thu Jun 21 14:49:21 2018 +0200 @@ -1269,7 +1269,7 @@ val thy = Toplevel.theory_of st; val ctxt = Toplevel.context_of st; fun pretty_thm (a, th) = Proof_Context.pretty_fact ctxt (a, [th]); - val check = Theory.check ctxt; + val check = Theory.check {long = false} ctxt; in Thm_Deps.unused_thms (case opt_range of diff -r fb6afa538b04 -r cb84beb84ca9 src/Pure/Thy/document_antiquotations.ML --- a/src/Pure/Thy/document_antiquotations.ML Thu Jun 21 14:29:44 2018 +0200 +++ b/src/Pure/Thy/document_antiquotations.ML Thu Jun 21 14:49:21 2018 +0200 @@ -60,7 +60,8 @@ fun pretty_prf full ctxt = Proof_Syntax.pretty_clean_proof_of ctxt full; -fun pretty_theory ctxt (name, pos) = (Theory.check ctxt (name, pos); Pretty.str name); +fun pretty_theory ctxt (name, pos) = + (Theory.check {long = false} ctxt (name, pos); Pretty.str name); val basic_entity = Thy_Output.antiquotation_pretty_source; diff -r fb6afa538b04 -r cb84beb84ca9 src/Pure/Thy/thy_output.ML --- a/src/Pure/Thy/thy_output.ML Thu Jun 21 14:29:44 2018 +0200 +++ b/src/Pure/Thy/thy_output.ML Thu Jun 21 14:49:21 2018 +0200 @@ -246,7 +246,7 @@ let val ctxt' = Toplevel.presentation_context state' - handle Toplevel.UNDEF => Proof_Context.init_global (Context.get_theory thy Context.PureN); + handle Toplevel.UNDEF => Proof_Context.get_global thy Context.PureN; val present = fold (fn (tok, (flag, 0)) => fold cons (present_token ctxt' tok) #> cons (Latex.string flag) diff -r fb6afa538b04 -r cb84beb84ca9 src/Pure/Tools/thm_deps.ML --- a/src/Pure/Tools/thm_deps.ML Thu Jun 21 14:29:44 2018 +0200 +++ b/src/Pure/Tools/thm_deps.ML Thu Jun 21 14:49:21 2018 +0200 @@ -27,7 +27,7 @@ val session = (case prefix of a :: _ => - (case try (Context.get_theory thy) a of + (case try (Context.get_theory {long = false} thy) a of SOME thy => (case Present.theory_qualifier thy of "" => [] diff -r fb6afa538b04 -r cb84beb84ca9 src/Pure/Tools/thy_deps.ML --- a/src/Pure/Tools/thy_deps.ML Thu Jun 21 14:29:44 2018 +0200 +++ b/src/Pure/Tools/thy_deps.ML Thu Jun 21 14:49:21 2018 +0200 @@ -36,6 +36,6 @@ let val thy0 = Proof_Context.theory_of ctxt in if Context.subthy (thy, thy0) then thy else raise THEORY ("Bad theory", [thy, thy0]) end); -val thy_deps_cmd = Graph_Display.display_graph oo gen_thy_deps Theory.check; +val thy_deps_cmd = Graph_Display.display_graph oo gen_thy_deps (Theory.check {long = false}); end; diff -r fb6afa538b04 -r cb84beb84ca9 src/Pure/context.ML --- a/src/Pure/context.ML Thu Jun 21 14:29:44 2018 +0200 +++ b/src/Pure/context.ML Thu Jun 21 14:49:21 2018 +0200 @@ -37,11 +37,11 @@ val theory_id_name: theory_id -> string val theory_long_name: theory -> string val theory_name: theory -> string + val theory_name': {long: bool} -> theory -> string val PureN: string val pretty_thy: theory -> Pretty.T val pretty_abbrev_thy: theory -> Pretty.T - val get_theory: theory -> string -> theory - val this_theory: theory -> string -> theory + val get_theory: {long: bool} -> theory -> string -> theory val eq_thy_id: theory_id * theory_id -> bool val eq_thy: theory * theory -> bool val proper_subthy_id: theory_id * theory_id -> bool @@ -160,6 +160,7 @@ val theory_id_name = Long_Name.base_name o theory_id_long_name; val theory_long_name = #name o history_of; val theory_name = Long_Name.base_name o theory_long_name; +fun theory_name' {long} = if long then theory_long_name else theory_name; val parents_of = #parents o ancestry_of; val ancestors_of = #ancestors o ancestry_of; @@ -191,18 +192,14 @@ val abbrev = if n > 5 then "..." :: List.drop (names, n - 5) else names; in Pretty.str_list "{" "}" abbrev end; -fun get_theory thy name = - if theory_name thy <> name then - (case find_first (fn thy' => theory_name thy' = name) (ancestors_of thy) of +fun get_theory long thy name = + if theory_name' long thy <> name then + (case find_first (fn thy' => theory_name' long thy' = name) (ancestors_of thy) of SOME thy' => thy' | NONE => error ("Unknown ancestor theory " ^ quote name)) else if #stage (history_of thy) = finished then thy else error ("Unfinished theory " ^ quote name); -fun this_theory thy name = - if theory_name thy = name then thy - else get_theory thy name; - (* build ids *) @@ -472,7 +469,7 @@ struct fun theory_of (Proof.Context (_, thy)) = thy; fun init_global thy = Proof.Context (init_data thy, thy); - fun get_global thy name = init_global (get_theory thy name); + fun get_global thy name = init_global (get_theory {long = false} thy name); end; structure Proof_Data = diff -r fb6afa538b04 -r cb84beb84ca9 src/Pure/theory.ML --- a/src/Pure/theory.ML Thu Jun 21 14:29:44 2018 +0200 +++ b/src/Pure/theory.ML Thu Jun 21 14:49:21 2018 +0200 @@ -14,7 +14,7 @@ val install_pure: theory -> unit val get_pure: unit -> theory val get_markup: theory -> Markup.T - val check: Proof.context -> string * Position.T -> theory + val check: {long: bool} -> Proof.context -> string * Position.T -> theory val axiom_table: theory -> term Name_Space.table val axiom_space: theory -> Name_Space.T val axioms_of: theory -> (string * term) list @@ -132,17 +132,17 @@ let val {pos, id, ...} = rep_theory thy in theory_markup false (Context.theory_name thy) id pos end; -fun check ctxt (name, pos) = +fun check long ctxt (name, pos) = let val thy = Proof_Context.theory_of ctxt; val thy' = - Context.get_theory thy name + Context.get_theory long thy name handle ERROR msg => let val completion = Completion.make (name, pos) (fn completed => - map Context.theory_name (ancestors_of thy) + map (Context.theory_name' long) (ancestors_of thy) |> filter completed |> sort_strings |> map (fn a => (a, (Markup.theoryN, a)))); diff -r fb6afa538b04 -r cb84beb84ca9 src/Tools/Code/code_thingol.ML --- a/src/Tools/Code/code_thingol.ML Thu Jun 21 14:29:44 2018 +0200 +++ b/src/Tools/Code/code_thingol.ML Thu Jun 21 14:49:21 2018 +0200 @@ -942,6 +942,10 @@ fun read_const_exprs_internal ctxt = let val thy = Proof_Context.theory_of ctxt; + fun this_theory name = + if Context.theory_name thy = name then thy + else Context.get_theory {long = false} thy name; + fun consts_of thy' = fold (fn (c, (_, NONE)) => cons c | _ => I) (#constants (Consts.dest (Sign.consts_of thy'))) [] @@ -954,7 +958,7 @@ SOME "_" => ([], consts_of thy) | SOME s => if String.isSuffix "._" s - then ([], consts_of_select (Context.this_theory thy (unsuffix "._" s))) + then ([], consts_of_select (this_theory (unsuffix "._" s))) else ([Code.read_const thy str], []) | NONE => ([Code.read_const thy str], [])); in apply2 flat o split_list o map read_const_expr end;