1.1 --- a/src/Pure/General/markup.ML Tue Mar 24 14:09:24 2009 +0100
1.2 +++ b/src/Pure/General/markup.ML Tue Mar 24 16:11:42 2009 +0100
1.3 @@ -70,6 +70,9 @@
1.4 val ML_stringN: string val ML_string: T
1.5 val ML_commentN: string val ML_comment: T
1.6 val ML_malformedN: string val ML_malformed: T
1.7 + val ML_defN: string val ML_def: T
1.8 + val ML_refN: string val ML_ref: T
1.9 + val ML_typingN: string val ML_typing: T
1.10 val ML_sourceN: string val ML_source: T
1.11 val doc_sourceN: string val doc_source: T
1.12 val antiqN: string val antiq: T
1.13 @@ -232,6 +235,10 @@
1.14 val (ML_commentN, ML_comment) = markup_elem "ML_comment";
1.15 val (ML_malformedN, ML_malformed) = markup_elem "ML_malformed";
1.16
1.17 +val (ML_defN, ML_def) = markup_elem "ML_def";
1.18 +val (ML_refN, ML_ref) = markup_elem "ML_ref";
1.19 +val (ML_typingN, ML_typing) = markup_elem "ML_typing";
1.20 +
1.21
1.22 (* embedded source text *)
1.23
2.1 --- a/src/Pure/General/markup.scala Tue Mar 24 14:09:24 2009 +0100
2.2 +++ b/src/Pure/General/markup.scala Tue Mar 24 16:11:42 2009 +0100
2.3 @@ -91,6 +91,10 @@
2.4 val ML_COMMENT = "ML_comment"
2.5 val ML_MALFORMED = "ML_malformed"
2.6
2.7 + val ML_DEF = "ML_def"
2.8 + val ML_REF = "ML_ref"
2.9 + val ML_TYPING = "ML_typing"
2.10 +
2.11
2.12 /* outer syntax */
2.13
3.1 --- a/src/Pure/Isar/isar_syn.ML Tue Mar 24 14:09:24 2009 +0100
3.2 +++ b/src/Pure/Isar/isar_syn.ML Tue Mar 24 16:11:42 2009 +0100
3.3 @@ -295,28 +295,28 @@
3.4
3.5 (* use ML text *)
3.6
3.7 -fun inherit_env (context as Context.Proof lthy) =
3.8 +fun propagate_env (context as Context.Proof lthy) =
3.9 Context.Proof (LocalTheory.map_contexts (ML_Context.inherit_env context) lthy)
3.10 - | inherit_env context = context;
3.11 + | propagate_env context = context;
3.12
3.13 -fun inherit_env_prf prf = Proof.map_contexts
3.14 +fun propagate_env_prf prf = Proof.map_contexts
3.15 (Context.proof_map (ML_Context.inherit_env (Context.Proof (Proof.context_of prf)))) prf;
3.16
3.17 val _ =
3.18 OuterSyntax.command "use" "ML text from file" (K.tag_ml K.thy_decl)
3.19 - (P.path >> (fn path => Toplevel.generic_theory (ThyInfo.exec_file false path #> inherit_env)));
3.20 + (P.path >> (fn path => Toplevel.generic_theory (ThyInfo.exec_file false path #> propagate_env)));
3.21
3.22 val _ =
3.23 OuterSyntax.command "ML" "ML text within theory or local theory" (K.tag_ml K.thy_decl)
3.24 (P.ML_source >> (fn (txt, pos) =>
3.25 Toplevel.generic_theory
3.26 - (ML_Context.exec (fn () => ML_Context.eval true pos txt) #> inherit_env)));
3.27 + (ML_Context.exec (fn () => ML_Context.eval true pos txt) #> propagate_env)));
3.28
3.29 val _ =
3.30 OuterSyntax.command "ML_prf" "ML text within proof" (K.tag_proof K.prf_decl)
3.31 (P.ML_source >> (fn (txt, pos) =>
3.32 Toplevel.proof (Proof.map_context (Context.proof_map
3.33 - (ML_Context.exec (fn () => ML_Context.eval true pos txt))) #> inherit_env_prf)));
3.34 + (ML_Context.exec (fn () => ML_Context.eval true pos txt))) #> propagate_env_prf)));
3.35
3.36 val _ =
3.37 OuterSyntax.command "ML_val" "diagnostic ML text" (K.tag_ml K.diag)
4.1 --- a/src/Pure/ML/ml_test.ML Tue Mar 24 14:09:24 2009 +0100
4.2 +++ b/src/Pure/ML/ml_test.ML Tue Mar 24 16:11:42 2009 +0100
4.3 @@ -6,63 +6,92 @@
4.4
4.5 signature ML_TEST =
4.6 sig
4.7 - val get_result: Proof.context -> PolyML.parseTree list
4.8 val eval: bool -> Position.T -> ML_Lex.token list -> unit
4.9 end
4.10
4.11 structure ML_Test: ML_TEST =
4.12 struct
4.13
4.14 -(* eval ML source tokens *)
4.15 +(* extra ML environment *)
4.16
4.17 -structure Result = GenericDataFun
4.18 +structure Extra_Env = GenericDataFun
4.19 (
4.20 - type T = PolyML.parseTree list;
4.21 - val empty = [];
4.22 - fun extend _ = [];
4.23 - fun merge _ _ = [];
4.24 + type T = Position.T Inttab.table; (*position of registered tokens*)
4.25 + val empty = Inttab.empty;
4.26 + val extend = I;
4.27 + fun merge _ = Inttab.merge (K true);
4.28 );
4.29
4.30 -val get_result = Result.get o Context.Proof;
4.31 +fun inherit_env context =
4.32 + ML_Context.inherit_env context #>
4.33 + Extra_Env.put (Extra_Env.get context);
4.34
4.35 +fun register_tokens toks context =
4.36 + let
4.37 + val regs = map (fn tok => (serial (), tok)) toks;
4.38 + val context' = context
4.39 + |> Extra_Env.map (fold (fn (i, tok) => Inttab.update (i, ML_Lex.pos_of tok)) regs);
4.40 + in (regs, context') end;
4.41 +
4.42 +fun pos_of_location context
4.43 + ({file, startLine = line, startPosition = i, endPosition = j, ...}: location) =
4.44 + (case pairself (Inttab.lookup (Extra_Env.get context)) (i, j) of
4.45 + (SOME pos1, SOME pos2) => Position.encode_range (pos1, pos2)
4.46 + | (SOME pos, NONE) => pos
4.47 + | _ => Position.line_file line file);
4.48 +
4.49 +
4.50 +(* parse trees *)
4.51 +
4.52 +fun report_parse_tree context =
4.53 + let
4.54 + val pos_of = pos_of_location context;
4.55 + fun report loc (PTtype types) = (* FIXME body text *)
4.56 + Position.report Markup.ML_typing (pos_of loc)
4.57 + | report loc (PTdeclaredAt decl) =
4.58 + Markup.markup (Markup.properties (Position.properties_of (pos_of decl)) Markup.ML_def) ""
4.59 + |> Position.report_text Markup.ML_ref (pos_of loc)
4.60 + | report _ (PTnextSibling tree) = report_tree (tree ())
4.61 + | report _ (PTfirstChild tree) = report_tree (tree ())
4.62 + | report _ _ = ()
4.63 + and report_tree (loc, props) = List.app (report loc) props;
4.64 + in report_tree end;
4.65 +
4.66 +
4.67 +(* eval ML source tokens *)
4.68
4.69 fun use_text ({name_space = space, print, error, ...}: use_context) verbose pos toks =
4.70 let
4.71 (* input *)
4.72
4.73 - val input = toks |> map (fn tok =>
4.74 - (serial (), (String.explode (ML_Lex.text_of tok), ML_Lex.pos_of tok)));
4.75 - val index_pos = Inttab.lookup (Inttab.make (map (apsnd snd) input));
4.76 + val input = Context.>>> (register_tokens toks);
4.77 + val input_buffer = ref (map (apsnd (String.explode o ML_Lex.text_of)) input);
4.78
4.79 - fun pos_of ({file, startLine = line, startPosition = i, endPosition = j, ...}: location) =
4.80 - (case (index_pos i, index_pos j) of
4.81 - (SOME p, SOME q) => Position.encode_range (p, q)
4.82 - | (SOME p, NONE) => p
4.83 - | _ => Position.line_file line file);
4.84 + val current_line = ref (the_default 1 (Position.line_of pos));
4.85
4.86 - val in_buffer = ref (map (apsnd fst) input);
4.87 - val current_line = ref (the_default 1 (Position.line_of pos));
4.88 + fun get_index () =
4.89 + the_default 0 (get_first (fn (_, []) => NONE | (i, _) => SOME i) (! input_buffer));
4.90 +
4.91 fun get () =
4.92 - (case ! in_buffer of
4.93 + (case ! input_buffer of
4.94 [] => NONE
4.95 - | (_, []) :: rest => (in_buffer := rest; get ())
4.96 + | (_, []) :: rest => (input_buffer := rest; get ())
4.97 | (i, c :: cs) :: rest =>
4.98 - (in_buffer := (i, cs) :: rest;
4.99 + (input_buffer := (i, cs) :: rest;
4.100 if c = #"\n" then current_line := ! current_line + 1 else ();
4.101 SOME c));
4.102 - fun get_index () = (case ! in_buffer of [] => 0 | (i, _) :: _ => i);
4.103
4.104
4.105 (* output *)
4.106
4.107 - val out_buffer = ref ([]: string list);
4.108 - fun output () = implode (rev (! out_buffer));
4.109 - fun put s = out_buffer := s :: ! out_buffer;
4.110 + val output_buffer = ref Buffer.empty;
4.111 + fun output () = Buffer.content (! output_buffer);
4.112 + fun put s = change output_buffer (Buffer.add s);
4.113
4.114 fun put_message {message, hard, location, context = _} =
4.115 (put (if hard then "Error: " else "Warning: ");
4.116 put (Pretty.string_of (Pretty.from_ML (pretty_ml message)));
4.117 - put (Position.str_of (pos_of location) ^ "\n"));
4.118 + put (Position.str_of (pos_of_location (the (Context.thread_data ())) location) ^ "\n"));
4.119
4.120
4.121 (* results *)
4.122 @@ -112,9 +141,11 @@
4.123 List.app apply_val values
4.124 end;
4.125
4.126 - fun result_fun (parse_tree, code) () =
4.127 - (Context.>> (Result.map (append (the_list parse_tree)));
4.128 - (case code of NONE => error "Static Errors" | SOME result => apply_result (result ())));
4.129 + fun result_fun (phase1, phase2) () =
4.130 + (case phase1 of NONE => ()
4.131 + | SOME parse_tree => report_parse_tree (the (Context.thread_data ())) parse_tree;
4.132 + case phase2 of NONE => error "Static Errors"
4.133 + | SOME code => apply_result (Toplevel.program code));
4.134
4.135
4.136 (* compiler invocation *)
4.137 @@ -124,12 +155,11 @@
4.138 PolyML.Compiler.CPNameSpace space,
4.139 PolyML.Compiler.CPErrorMessageProc put_message,
4.140 PolyML.Compiler.CPLineNo (fn () => ! current_line),
4.141 + PolyML.Compiler.CPFileName (the_default "ML" (Position.file_of pos)),
4.142 PolyML.Compiler.CPLineOffset get_index,
4.143 - PolyML.Compiler.CPFileName (the_default "ML" (Position.file_of pos)),
4.144 - PolyML.Compiler.CPPrintInAlphabeticalOrder false,
4.145 PolyML.Compiler.CPCompilerResultFun result_fun];
4.146 val _ =
4.147 - (while not (List.null (! in_buffer)) do
4.148 + (while not (List.null (! input_buffer)) do
4.149 PolyML.compiler (get, parameters) ())
4.150 handle exn =>
4.151 (put ("Exception- " ^ General.exnMessage exn ^ " raised");
4.152 @@ -149,7 +179,7 @@
4.153
4.154 val _ = Context.setmp_thread_data env_ctxt
4.155 (fn () => (eval false Position.none env; Context.thread_data ())) ()
4.156 - |> (fn NONE => () | SOME context' => Context.>> (ML_Context.inherit_env context'));
4.157 + |> (fn NONE => () | SOME context' => Context.>> (inherit_env context'));
4.158 val _ = eval true pos body;
4.159 val _ = eval false Position.none (ML_Lex.tokenize "structure Isabelle = struct end");
4.160 in () end;
4.161 @@ -157,14 +187,14 @@
4.162
4.163 local structure P = OuterParse and K = OuterKeyword in
4.164
4.165 -fun inherit_env (context as Context.Proof lthy) =
4.166 - Context.Proof (LocalTheory.map_contexts (ML_Context.inherit_env context) lthy)
4.167 - | inherit_env context = context;
4.168 +fun propagate_env (context as Context.Proof lthy) =
4.169 + Context.Proof (LocalTheory.map_contexts (inherit_env context) lthy)
4.170 + | propagate_env context = context;
4.171
4.172 val _ =
4.173 OuterSyntax.command "ML_test" "advanced ML compiler test" (K.tag_ml K.thy_decl)
4.174 (P.ML_source >> (fn src =>
4.175 - Toplevel.generic_theory (ML_Context.exec (fn () => ML_test src) #> inherit_env)));
4.176 + Toplevel.generic_theory (ML_Context.exec (fn () => ML_test src) #> propagate_env)));
4.177
4.178 end;
4.179