some support for inlining file content into outer syntax token language;
authorwenzelm
Mon Aug 20 17:05:53 2012 +0200 (2012-08-20)
changeset 48867e9beabf045ab
parent 48866 034df7b05759
child 48868 aeea516440c8
some support for inlining file content into outer syntax token language;
etc/isar-keywords-ZF.el
etc/isar-keywords.el
src/Pure/Isar/keyword.ML
src/Pure/Isar/keyword.scala
src/Pure/Isar/token.ML
src/Pure/ROOT.ML
src/Pure/System/build.scala
src/Pure/Thy/thy_load.ML
src/Pure/Thy/thy_syntax.ML
     1.1 --- a/etc/isar-keywords-ZF.el	Mon Aug 20 15:43:10 2012 +0200
     1.2 +++ b/etc/isar-keywords-ZF.el	Mon Aug 20 17:05:53 2012 +0200
     1.3 @@ -10,6 +10,7 @@
     1.4      "Isabelle\\.command"
     1.5      "ML"
     1.6      "ML_command"
     1.7 +    "ML_file"
     1.8      "ML_prf"
     1.9      "ML_val"
    1.10      "ProofGeneral\\.inform_file_processed"
    1.11 @@ -343,6 +344,7 @@
    1.12  
    1.13  (defconst isar-keywords-theory-decl
    1.14    '("ML"
    1.15 +    "ML_file"
    1.16      "abbreviation"
    1.17      "arities"
    1.18      "attribute_setup"
     2.1 --- a/etc/isar-keywords.el	Mon Aug 20 15:43:10 2012 +0200
     2.2 +++ b/etc/isar-keywords.el	Mon Aug 20 17:05:53 2012 +0200
     2.3 @@ -10,6 +10,7 @@
     2.4      "Isabelle\\.command"
     2.5      "ML"
     2.6      "ML_command"
     2.7 +    "ML_file"
     2.8      "ML_prf"
     2.9      "ML_val"
    2.10      "ProofGeneral\\.inform_file_processed"
    2.11 @@ -453,6 +454,7 @@
    2.12  
    2.13  (defconst isar-keywords-theory-decl
    2.14    '("ML"
    2.15 +    "ML_file"
    2.16      "abbreviation"
    2.17      "arities"
    2.18      "atom_decl"
     3.1 --- a/src/Pure/Isar/keyword.ML	Mon Aug 20 15:43:10 2012 +0200
     3.2 +++ b/src/Pure/Isar/keyword.ML	Mon Aug 20 17:05:53 2012 +0200
     3.3 @@ -50,6 +50,7 @@
     3.4    val get_lexicons: unit -> Scan.lexicon * Scan.lexicon
     3.5    val is_keyword: string -> bool
     3.6    val command_keyword: string -> T option
     3.7 +  val command_files: string -> string list
     3.8    val command_tags: string -> string list
     3.9    val dest: unit -> string list * string list
    3.10    val status: unit -> unit
    3.11 @@ -59,6 +60,7 @@
    3.12    val is_regular: string -> bool
    3.13    val is_heading: string -> bool
    3.14    val is_theory_begin: string -> bool
    3.15 +  val is_theory_load: string -> bool
    3.16    val is_theory: string -> bool
    3.17    val is_proof: string -> bool
    3.18    val is_theory_goal: string -> bool
    3.19 @@ -96,9 +98,9 @@
    3.20  val thy_heading2 = kind "thy_heading2";
    3.21  val thy_heading3 = kind "thy_heading3";
    3.22  val thy_heading4 = kind "thy_heading4";
    3.23 +val thy_decl = kind "thy_decl";
    3.24  val thy_load = kind "thy_load";
    3.25  fun thy_load_files files = Keyword {kind = "thy_load", files = files, tags = []};
    3.26 -val thy_decl = kind "thy_decl";
    3.27  val thy_script = kind "thy_script";
    3.28  val thy_goal = kind "thy_goal";
    3.29  val thy_schematic_goal = kind "thy_schematic_goal";
    3.30 @@ -193,7 +195,8 @@
    3.31    in Scan.is_literal minor syms orelse Scan.is_literal major syms end;
    3.32  
    3.33  fun command_keyword name = Symtab.lookup (get_commands ()) name;
    3.34 -fun command_tags name = these (Option.map tags_of (command_keyword name));
    3.35 +val command_files = these o Option.map (#2 o kind_files_of) o command_keyword;
    3.36 +val command_tags = these o Option.map tags_of o command_keyword;
    3.37  
    3.38  fun dest () = pairself (sort_strings o Scan.dest_lexicon) (get_lexicons ());
    3.39  
    3.40 @@ -242,6 +245,8 @@
    3.41  
    3.42  val is_theory_begin = command_category [thy_begin];
    3.43  
    3.44 +val is_theory_load = command_category [thy_load];
    3.45 +
    3.46  val is_theory = command_category
    3.47    [thy_begin, thy_end, thy_heading1, thy_heading2, thy_heading3, thy_heading4,
    3.48      thy_load, thy_decl, thy_script, thy_goal, thy_schematic_goal];
     4.1 --- a/src/Pure/Isar/keyword.scala	Mon Aug 20 15:43:10 2012 +0200
     4.2 +++ b/src/Pure/Isar/keyword.scala	Mon Aug 20 17:05:53 2012 +0200
     4.3 @@ -21,6 +21,7 @@
     4.4    val THY_HEADING3 = "thy_heading3"
     4.5    val THY_HEADING4 = "thy_heading4"
     4.6    val THY_DECL = "thy_decl"
     4.7 +  val THY_LOAD = "thy_load"
     4.8    val THY_SCRIPT = "thy_script"
     4.9    val THY_GOAL = "thy_goal"
    4.10    val THY_SCHEMATIC_GOAL = "thy_schematic_goal"
     5.1 --- a/src/Pure/Isar/token.ML	Mon Aug 20 15:43:10 2012 +0200
     5.2 +++ b/src/Pure/Isar/token.ML	Mon Aug 20 17:05:53 2012 +0200
     5.3 @@ -10,9 +10,10 @@
     5.4      Command | Keyword | Ident | LongIdent | SymIdent | Var | TypeIdent | TypeVar |
     5.5      Nat | Float | String | AltString | Verbatim | Space | Comment | InternalValue |
     5.6      Error of string | Sync | EOF
     5.7 +  type files = Path.T * (string * Position.T) list
     5.8    datatype value =
     5.9      Text of string | Typ of typ | Term of term | Fact of thm list |
    5.10 -    Attribute of morphism -> attribute
    5.11 +    Attribute of morphism -> attribute | Files of files
    5.12    type T
    5.13    val str_of_kind: kind -> string
    5.14    val position_of: T -> Position.T
    5.15 @@ -28,6 +29,7 @@
    5.16    val keyword_with: (string -> bool) -> T -> bool
    5.17    val ident_with: (string -> bool) -> T -> bool
    5.18    val is_command: T -> bool
    5.19 +  val is_name: T -> bool
    5.20    val is_proper: T -> bool
    5.21    val is_semicolon: T -> bool
    5.22    val is_comment: T -> bool
    5.23 @@ -42,6 +44,8 @@
    5.24    val content_of: T -> string
    5.25    val unparse: T -> string
    5.26    val text_of: T -> string * string
    5.27 +  val get_files: T -> files option
    5.28 +  val put_files: files -> T -> T
    5.29    val get_value: T -> value option
    5.30    val map_value: (value -> value) -> T -> T
    5.31    val mk_text: string -> T
    5.32 @@ -74,12 +78,15 @@
    5.33    args.ML).  Note that an assignable ref designates an intermediate
    5.34    state of internalization -- it is NOT meant to persist.*)
    5.35  
    5.36 +type files = Path.T * (string * Position.T) list;  (*master dir, multiple file content*)
    5.37 +
    5.38  datatype value =
    5.39    Text of string |
    5.40    Typ of typ |
    5.41    Term of term |
    5.42    Fact of thm list |
    5.43 -  Attribute of morphism -> attribute;
    5.44 +  Attribute of morphism -> attribute |
    5.45 +  Files of files;
    5.46  
    5.47  datatype slot =
    5.48    Slot |
    5.49 @@ -149,6 +156,7 @@
    5.50  fun is_kind k (Token (_, (k', _), _)) = k = k';
    5.51  
    5.52  val is_command = is_kind Command;
    5.53 +val is_name = is_kind Ident orf is_kind SymIdent orf is_kind String orf is_kind Nat;
    5.54  
    5.55  fun keyword_with pred (Token (_, (Keyword, x), _)) = pred x
    5.56    | keyword_with _ _ = false;
    5.57 @@ -229,6 +237,16 @@
    5.58  
    5.59  (** associated values **)
    5.60  
    5.61 +(* inlined file content *)
    5.62 +
    5.63 +fun get_files (Token (_, _, Value (SOME (Files files)))) = SOME files
    5.64 +  | get_files _ = NONE;
    5.65 +
    5.66 +fun put_files files (Token (x, y, Slot)) = Token (x, y, Value (SOME (Files files)))
    5.67 +  | put_files _ tok =
    5.68 +      raise Fail ("Cannot put inlined files here" ^ Position.str_of (position_of tok));
    5.69 +
    5.70 +
    5.71  (* access values *)
    5.72  
    5.73  fun get_value (Token (_, _, Value v)) = v
     6.1 --- a/src/Pure/ROOT.ML	Mon Aug 20 15:43:10 2012 +0200
     6.2 +++ b/src/Pure/ROOT.ML	Mon Aug 20 17:05:53 2012 +0200
     6.3 @@ -321,6 +321,16 @@
     6.4          Toplevel.init_theory
     6.5            (fn () => Thy_Info.toplevel_begin_theory (Thy_Load.get_master_path ()) header)));
     6.6  
     6.7 +val _ =
     6.8 +  Outer_Syntax.command
     6.9 +    (("ML_file", Keyword.tag_ml Keyword.thy_load), Position.none) "ML text from file"
    6.10 +    (Thy_Load.parse_files "ML_file" >> (fn files => Toplevel.generic_theory (fn gthy =>
    6.11 +      let val (_, [(txt, pos)]) = files (Context.theory_of gthy) in
    6.12 +        gthy
    6.13 +        |> ML_Context.exec (fn () => ML_Context.eval_text true pos txt)
    6.14 +        |> Local_Theory.propagate_ml_env
    6.15 +      end)));
    6.16 +
    6.17  Unsynchronized.setmp Multithreading.max_threads 1
    6.18    use_thy "Pure";
    6.19  Context.set_thread_data NONE;
     7.1 --- a/src/Pure/System/build.scala	Mon Aug 20 15:43:10 2012 +0200
     7.2 +++ b/src/Pure/System/build.scala	Mon Aug 20 17:05:53 2012 +0200
     7.3 @@ -341,6 +341,7 @@
     7.4                    Outer_Syntax.init() +
     7.5                      // FIXME avoid hardwired stuff!?
     7.6                      ("theory", Keyword.THY_BEGIN) +
     7.7 +                    ("ML_file", Keyword.THY_LOAD) +
     7.8                      ("hence", (Keyword.PRF_ASM_GOAL, Nil), "then have") +
     7.9                      ("thus", (Keyword.PRF_ASM_GOAL, Nil), "then show")
    7.10                  (Set.empty[String], init_syntax, Nil)
     8.1 --- a/src/Pure/Thy/thy_load.ML	Mon Aug 20 15:43:10 2012 +0200
     8.2 +++ b/src/Pure/Thy/thy_load.ML	Mon Aug 20 17:05:53 2012 +0200
     8.3 @@ -22,6 +22,8 @@
     8.4    val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory
     8.5    val load_thy: int -> Path.T -> Thy_Header.header -> Position.T -> string ->
     8.6      theory list -> theory * unit future
     8.7 +  val resolve_files: Path.T -> Thy_Syntax.span -> Thy_Syntax.span
     8.8 +  val parse_files: string -> (theory -> Token.files) parser
     8.9    val set_master_path: Path.T -> unit
    8.10    val get_master_path: unit -> Path.T
    8.11  end;
    8.12 @@ -158,6 +160,42 @@
    8.13  fun exec_ml src_path = ML_Context.exec (fn () => use_ml src_path);
    8.14  
    8.15  
    8.16 +(* inlined files *)
    8.17 +
    8.18 +fun read_files cmd dir tok =
    8.19 +  let
    8.20 +    val path = Path.explode (Token.content_of tok);
    8.21 +    val exts = Keyword.command_files cmd;
    8.22 +    val variants =
    8.23 +      if null exts then [path]
    8.24 +      else map (fn ext => Path.ext ext path) exts;
    8.25 +  in (dir, variants |> map (Path.append dir #> (fn p => (File.read p, Path.position p)))) end;
    8.26 +
    8.27 +fun resolve_files dir (span as Thy_Syntax.Span (Thy_Syntax.Command cmd, toks)) =
    8.28 +      if Keyword.is_theory_load cmd then
    8.29 +        (case find_index Token.is_name (rev toks) of  (* FIXME allow trailing cmt (!?!) *)
    8.30 +          ~1 => span
    8.31 +        | i' =>
    8.32 +            let
    8.33 +              val i = length toks - 1 - i';
    8.34 +              val toks' = toks |> map_index (fn (j, tok) =>
    8.35 +                if i = j then Token.put_files (read_files cmd dir tok) tok
    8.36 +                else tok);
    8.37 +            in Thy_Syntax.Span (Thy_Syntax.Command cmd, toks') end)
    8.38 +      else span
    8.39 +  | resolve_files _ span = span;
    8.40 +
    8.41 +fun parse_files cmd =
    8.42 +  Scan.ahead Parse.not_eof -- Parse.group (fn () => "file name/path specification") Parse.name
    8.43 +    >> (fn (tok, name) => fn thy =>
    8.44 +      (case Token.get_files tok of
    8.45 +        SOME files => files
    8.46 +      | NONE =>
    8.47 +          (warning ("Dynamic loading of files: " ^ quote name ^
    8.48 +              Position.str_of (Token.position_of tok));
    8.49 +            read_files cmd (master_directory thy) tok)));
    8.50 +
    8.51 +
    8.52  (* load_thy *)
    8.53  
    8.54  fun begin_theory dir {name, imports, keywords, uses} parents =
    8.55 @@ -192,7 +230,7 @@
    8.56    let
    8.57      val time = ! Toplevel.timing;
    8.58  
    8.59 -    val {name, imports, uses, ...} = header;
    8.60 +    val {name, uses, ...} = header;
    8.61      val _ = Thy_Header.define_keywords header;
    8.62      val _ = Present.init_theory name;
    8.63      fun init () =
    8.64 @@ -202,7 +240,7 @@
    8.65      val lexs = Keyword.get_lexicons ();
    8.66  
    8.67      val toks = Thy_Syntax.parse_tokens lexs pos text;
    8.68 -    val spans = Thy_Syntax.parse_spans toks;
    8.69 +    val spans = map (resolve_files dir) (Thy_Syntax.parse_spans toks);
    8.70      val elements = Thy_Syntax.parse_elements spans;
    8.71  
    8.72      val _ = Present.theory_source name
     9.1 --- a/src/Pure/Thy/thy_syntax.ML	Mon Aug 20 15:43:10 2012 +0200
     9.2 +++ b/src/Pure/Thy/thy_syntax.ML	Mon Aug 20 17:05:53 2012 +0200
     9.3 @@ -10,7 +10,7 @@
     9.4    val reports_of_tokens: Token.T list -> bool * (Position.report * string) list
     9.5    val present_token: Token.T -> Output.output
     9.6    datatype span_kind = Command of string | Ignored | Malformed
     9.7 -  type span
     9.8 +  datatype span = Span of span_kind * Token.T list
     9.9    val span_kind: span -> span_kind
    9.10    val span_content: span -> Token.T list
    9.11    val present_span: span -> Output.output