src/Pure/PIDE/resources.ML
changeset 56208 06cc31dff138
parent 56204 f70e69208a8c
child 56286 7ede6ca96c61
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/PIDE/resources.ML	Tue Mar 18 17:39:03 2014 +0100
     1.3 @@ -0,0 +1,243 @@
     1.4 +(*  Title:      Pure/PIDE/resources.ML
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +Resources for theories and auxiliary files.
     1.8 +*)
     1.9 +
    1.10 +signature RESOURCES =
    1.11 +sig
    1.12 +  val master_directory: theory -> Path.T
    1.13 +  val imports_of: theory -> (string * Position.T) list
    1.14 +  val thy_path: Path.T -> Path.T
    1.15 +  val check_thy: Path.T -> string ->
    1.16 +   {master: Path.T * SHA1.digest, text: string, theory_pos: Position.T,
    1.17 +    imports: (string * Position.T) list, keywords: Thy_Header.keywords}
    1.18 +  val parse_files: string -> (theory -> Token.file list) parser
    1.19 +  val provide: Path.T * SHA1.digest -> theory -> theory
    1.20 +  val provide_parse_files: string -> (theory -> Token.file list * theory) parser
    1.21 +  val load_file: theory -> Path.T -> (Path.T * SHA1.digest) * string
    1.22 +  val loaded_files: theory -> Path.T list
    1.23 +  val loaded_files_current: theory -> bool
    1.24 +  val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory
    1.25 +  val load_thy: bool -> (Toplevel.transition -> Time.time option) -> int -> Path.T ->
    1.26 +    Thy_Header.header -> Position.T -> string -> theory list -> theory * (unit -> unit) * int
    1.27 +end;
    1.28 +
    1.29 +structure Resources: RESOURCES =
    1.30 +struct
    1.31 +
    1.32 +(* manage source files *)
    1.33 +
    1.34 +type files =
    1.35 + {master_dir: Path.T,  (*master directory of theory source*)
    1.36 +  imports: (string * Position.T) list,  (*source specification of imports*)
    1.37 +  provided: (Path.T * SHA1.digest) list};  (*source path, digest*)
    1.38 +
    1.39 +fun make_files (master_dir, imports, provided): files =
    1.40 + {master_dir = master_dir, imports = imports, provided = provided};
    1.41 +
    1.42 +structure Files = Theory_Data
    1.43 +(
    1.44 +  type T = files;
    1.45 +  val empty = make_files (Path.current, [], []);
    1.46 +  fun extend _ = empty;
    1.47 +  fun merge _ = empty;
    1.48 +);
    1.49 +
    1.50 +fun map_files f =
    1.51 +  Files.map (fn {master_dir, imports, provided} =>
    1.52 +    make_files (f (master_dir, imports, provided)));
    1.53 +
    1.54 +
    1.55 +val master_directory = #master_dir o Files.get;
    1.56 +val imports_of = #imports o Files.get;
    1.57 +
    1.58 +fun put_deps master_dir imports = map_files (fn _ => (master_dir, imports, []));
    1.59 +
    1.60 +
    1.61 +(* theory files *)
    1.62 +
    1.63 +val thy_path = Path.ext "thy";
    1.64 +
    1.65 +fun check_file dir file = File.check_file (File.full_path dir file);
    1.66 +
    1.67 +fun check_thy dir thy_name =
    1.68 +  let
    1.69 +    val path = thy_path (Path.basic thy_name);
    1.70 +    val master_file = check_file dir path;
    1.71 +    val text = File.read master_file;
    1.72 +
    1.73 +    val {name = (name, pos), imports, keywords} =
    1.74 +      Thy_Header.read (Path.position master_file) text;
    1.75 +    val _ = thy_name <> name andalso
    1.76 +      error ("Bad file name " ^ Path.print path ^ " for theory " ^ quote name ^ Position.here pos);
    1.77 +  in
    1.78 +   {master = (master_file, SHA1.digest text), text = text, theory_pos = pos,
    1.79 +    imports = imports, keywords = keywords}
    1.80 +  end;
    1.81 +
    1.82 +
    1.83 +(* load files *)
    1.84 +
    1.85 +fun parse_files cmd =
    1.86 +  Scan.ahead Parse.not_eof -- Parse.path >> (fn (tok, name) => fn thy =>
    1.87 +    (case Token.get_files tok of
    1.88 +      [] =>
    1.89 +        let
    1.90 +          val master_dir = master_directory thy;
    1.91 +          val pos = Token.pos_of tok;
    1.92 +          val src_paths = Keyword.command_files cmd (Path.explode name);
    1.93 +        in map (Command.read_file master_dir pos) src_paths end
    1.94 +    | files => map Exn.release files));
    1.95 +
    1.96 +fun provide (src_path, id) =
    1.97 +  map_files (fn (master_dir, imports, provided) =>
    1.98 +    if AList.defined (op =) provided src_path then
    1.99 +      error ("Duplicate use of source file: " ^ Path.print src_path)
   1.100 +    else (master_dir, imports, (src_path, id) :: provided));
   1.101 +
   1.102 +fun provide_parse_files cmd =
   1.103 +  parse_files cmd >> (fn files => fn thy =>
   1.104 +    let
   1.105 +      val fs = files thy;
   1.106 +      val thy' = fold (fn {src_path, digest, ...} => provide (src_path, digest)) fs thy;
   1.107 +    in (fs, thy') end);
   1.108 +
   1.109 +fun load_file thy src_path =
   1.110 +  let
   1.111 +    val full_path = check_file (master_directory thy) src_path;
   1.112 +    val text = File.read full_path;
   1.113 +    val id = SHA1.digest text;
   1.114 +  in ((full_path, id), text) end;
   1.115 +
   1.116 +fun loaded_files_current thy =
   1.117 +  #provided (Files.get thy) |>
   1.118 +    forall (fn (src_path, id) =>
   1.119 +      (case try (load_file thy) src_path of
   1.120 +        NONE => false
   1.121 +      | SOME ((_, id'), _) => id = id'));
   1.122 +
   1.123 +(*Proof General legacy*)
   1.124 +fun loaded_files thy =
   1.125 +  let val {master_dir, provided, ...} = Files.get thy
   1.126 +  in map (File.full_path master_dir o #1) provided end;
   1.127 +
   1.128 +
   1.129 +(* load theory *)
   1.130 +
   1.131 +fun begin_theory master_dir {name, imports, keywords} parents =
   1.132 +  Theory.begin_theory name parents
   1.133 +  |> put_deps master_dir imports
   1.134 +  |> fold Thy_Header.declare_keyword keywords;
   1.135 +
   1.136 +fun excursion master_dir last_timing init elements =
   1.137 +  let
   1.138 +    fun prepare_span span =
   1.139 +      Thy_Syntax.span_content span
   1.140 +      |> Command.read init master_dir []
   1.141 +      |> (fn tr => Toplevel.put_timing (last_timing tr) tr);
   1.142 +
   1.143 +    fun element_result span_elem (st, _) =
   1.144 +      let
   1.145 +        val elem = Thy_Syntax.map_element prepare_span span_elem;
   1.146 +        val (results, st') = Toplevel.element_result elem st;
   1.147 +        val pos' = Toplevel.pos_of (Thy_Syntax.last_element elem);
   1.148 +      in (results, (st', pos')) end;
   1.149 +
   1.150 +    val (results, (end_state, end_pos)) =
   1.151 +      fold_map element_result elements (Toplevel.toplevel, Position.none);
   1.152 +
   1.153 +    val thy = Toplevel.end_theory end_pos end_state;
   1.154 +  in (results, thy) end;
   1.155 +
   1.156 +fun load_thy document last_timing update_time master_dir header text_pos text parents =
   1.157 +  let
   1.158 +    val time = ! Toplevel.timing;
   1.159 +
   1.160 +    val {name = (name, _), ...} = header;
   1.161 +    val _ = Thy_Header.define_keywords header;
   1.162 +
   1.163 +    val lexs = Keyword.get_lexicons ();
   1.164 +    val toks = Thy_Syntax.parse_tokens lexs text_pos text;
   1.165 +    val spans = Thy_Syntax.parse_spans toks;
   1.166 +    val elements = Thy_Syntax.parse_elements spans;
   1.167 +
   1.168 +    fun init () =
   1.169 +      begin_theory master_dir header parents
   1.170 +      |> Present.begin_theory update_time
   1.171 +          (fn () => HTML.html_mode (implode o map Thy_Syntax.present_span) spans);
   1.172 +
   1.173 +    val _ = if time then writeln ("\n**** Starting theory " ^ quote name ^ " ****") else ();
   1.174 +    val (results, thy) =
   1.175 +      cond_timeit time "" (fn () => excursion master_dir last_timing init elements);
   1.176 +    val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else ();
   1.177 +
   1.178 +    fun present () =
   1.179 +      let
   1.180 +        val res = filter_out (Toplevel.is_ignored o #1) (maps Toplevel.join_results results);
   1.181 +        val ((minor, _), outer_syntax) = Outer_Syntax.get_syntax ();
   1.182 +      in
   1.183 +        if exists (Toplevel.is_skipped_proof o #2) res then
   1.184 +          warning ("Cannot present theory with skipped proofs: " ^ quote name)
   1.185 +        else
   1.186 +          let val tex_source =
   1.187 +            Thy_Output.present_thy minor Keyword.command_tags
   1.188 +              (Outer_Syntax.is_markup outer_syntax) res toks
   1.189 +            |> Buffer.content;
   1.190 +          in if document then Present.theory_output name tex_source else () end
   1.191 +      end;
   1.192 +
   1.193 +  in (thy, present, size text) end;
   1.194 +
   1.195 +
   1.196 +(* antiquotations *)
   1.197 +
   1.198 +local
   1.199 +
   1.200 +fun check_path strict ctxt dir (name, pos) =
   1.201 +  let
   1.202 +    val _ = Context_Position.report ctxt pos Markup.language_path;
   1.203 +
   1.204 +    val path = Path.append dir (Path.explode name)
   1.205 +      handle ERROR msg => error (msg ^ Position.here pos);
   1.206 +
   1.207 +    val _ = Context_Position.report ctxt pos (Markup.path (Path.smart_implode path));
   1.208 +    val _ =
   1.209 +      if can Path.expand path andalso File.exists path then ()
   1.210 +      else
   1.211 +        let
   1.212 +          val path' = perhaps (try Path.expand) path;
   1.213 +          val msg = "Bad file: " ^ Path.print path' ^ Position.here pos;
   1.214 +        in
   1.215 +          if strict then error msg
   1.216 +          else
   1.217 +            Context_Position.if_visible ctxt Output.report
   1.218 +              (Markup.markup (Markup.bad |> Markup.properties (Position.properties_of pos)) msg)
   1.219 +        end;
   1.220 +  in path end;
   1.221 +
   1.222 +fun file_antiq strict ctxt (name, pos) =
   1.223 +  let
   1.224 +    val dir = master_directory (Proof_Context.theory_of ctxt);
   1.225 +    val _ = check_path strict ctxt dir (name, pos);
   1.226 +  in
   1.227 +    space_explode "/" name
   1.228 +    |> map Thy_Output.verb_text
   1.229 +    |> space_implode (Thy_Output.verb_text "/" ^ "\\discretionary{}{}{}")
   1.230 +  end;
   1.231 +
   1.232 +in
   1.233 +
   1.234 +val _ = Theory.setup
   1.235 + (Thy_Output.antiquotation @{binding file} (Scan.lift (Parse.position Parse.path))
   1.236 +    (file_antiq true o #context) #>
   1.237 +  Thy_Output.antiquotation @{binding file_unchecked} (Scan.lift (Parse.position Parse.path))
   1.238 +    (file_antiq false o #context) #>
   1.239 +  ML_Antiquotation.value @{binding path}
   1.240 +    (Args.context -- Scan.lift (Parse.position Parse.path) >> (fn (ctxt, arg) =>
   1.241 +      let val path = check_path true ctxt Path.current arg
   1.242 +      in "Path.explode " ^ ML_Syntax.print_string (Path.implode path) end)));
   1.243 +
   1.244 +end;
   1.245 +
   1.246 +end;