src/Pure/PIDE/resources.ML
changeset 67219 81e9804b2014
parent 67217 53867014e299
child 67386 998e01d6f8fd
     1.1 --- a/src/Pure/PIDE/resources.ML	Sat Dec 16 20:02:40 2017 +0100
     1.2 +++ b/src/Pure/PIDE/resources.ML	Sat Dec 16 21:53:07 2017 +0100
     1.3 @@ -8,13 +8,15 @@
     1.4  sig
     1.5    val default_qualifier: string
     1.6    val init_session_base:
     1.7 -    {global_theories: (string * string) list,
     1.8 +    {sessions: string list,
     1.9 +     global_theories: (string * string) list,
    1.10       loaded_theories: string list,
    1.11       known_theories: (string * string) list} -> unit
    1.12    val finish_session_base: unit -> unit
    1.13    val global_theory: string -> string option
    1.14    val loaded_theory: string -> bool
    1.15    val known_theory: string -> Path.T option
    1.16 +  val check_session: Proof.context -> string * Position.T -> string
    1.17    val master_directory: theory -> Path.T
    1.18    val imports_of: theory -> (string * Position.T) list
    1.19    val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory
    1.20 @@ -42,24 +44,27 @@
    1.21  val default_qualifier = "Draft";
    1.22  
    1.23  val empty_session_base =
    1.24 -  {global_theories = Symtab.empty: string Symtab.table,
    1.25 +  {sessions = []: string list,
    1.26 +   global_theories = Symtab.empty: string Symtab.table,
    1.27     loaded_theories = Symtab.empty: unit Symtab.table,
    1.28     known_theories = Symtab.empty: Path.T Symtab.table};
    1.29  
    1.30  val global_session_base =
    1.31    Synchronized.var "Sessions.base" empty_session_base;
    1.32  
    1.33 -fun init_session_base {global_theories, loaded_theories, known_theories} =
    1.34 +fun init_session_base {sessions, global_theories, loaded_theories, known_theories} =
    1.35    Synchronized.change global_session_base
    1.36      (fn _ =>
    1.37 -      {global_theories = Symtab.make global_theories,
    1.38 +      {sessions = sort_strings sessions,
    1.39 +       global_theories = Symtab.make global_theories,
    1.40         loaded_theories = Symtab.make_set loaded_theories,
    1.41         known_theories = Symtab.make (map (apsnd Path.explode) known_theories)});
    1.42  
    1.43  fun finish_session_base () =
    1.44    Synchronized.change global_session_base
    1.45      (fn {global_theories, loaded_theories, ...} =>
    1.46 -      {global_theories = global_theories,
    1.47 +      {sessions = [],
    1.48 +       global_theories = global_theories,
    1.49         loaded_theories = loaded_theories,
    1.50         known_theories = #known_theories empty_session_base});
    1.51  
    1.52 @@ -69,6 +74,21 @@
    1.53  fun loaded_theory a = Symtab.defined (get_session_base #loaded_theories) a;
    1.54  fun known_theory a = Symtab.lookup (get_session_base #known_theories) a;
    1.55  
    1.56 +fun check_session ctxt (name, pos) =
    1.57 +  let val sessions = get_session_base #sessions in
    1.58 +    if member (op =) sessions name then
    1.59 +      (Context_Position.report ctxt pos (Markup.entity Markup.sessionN name); name)
    1.60 +    else
    1.61 +      let
    1.62 +        val completion =
    1.63 +          Completion.make (name, pos) (fn completed =>
    1.64 +              sessions
    1.65 +              |> filter completed
    1.66 +              |> map (fn a => (a, (Markup.sessionN, a))));
    1.67 +        val report = Markup.markup_report (Completion.reported_text completion);
    1.68 +      in error ("Bad session " ^ quote name ^ Position.here pos ^ report) end
    1.69 +  end;
    1.70 +
    1.71  
    1.72  (* manage source files *)
    1.73  
    1.74 @@ -237,7 +257,9 @@
    1.75  in
    1.76  
    1.77  val _ = Theory.setup
    1.78 - (Thy_Output.antiquotation \<^binding>\<open>path\<close> (Scan.lift (Parse.position Parse.path))
    1.79 + (Thy_Output.antiquotation \<^binding>\<open>session\<close> (Scan.lift (Parse.position Parse.embedded))
    1.80 +    (fn {context = ctxt, ...} => Thy_Output.verbatim_text ctxt o check_session ctxt) #>
    1.81 +  Thy_Output.antiquotation \<^binding>\<open>path\<close> (Scan.lift (Parse.position Parse.path))
    1.82      (document_antiq check_path o #context) #>
    1.83    Thy_Output.antiquotation \<^binding>\<open>file\<close> (Scan.lift (Parse.position Parse.path))
    1.84      (document_antiq check_file o #context) #>