--- a/src/Pure/Isar/isar_output.ML Mon Sep 05 17:38:20 2005 +0200
+++ b/src/Pure/Isar/isar_output.ML Mon Sep 05 17:38:21 2005 +0200
@@ -206,7 +206,7 @@
(* command spans *)
type command = string * Position.T * string list; (*name, position, tags*)
-type tok = token * string * int; (*token, markup flag, meta-comment depth*)
+type tok = token * string * int; (*token, markup flag, meta-comment depth*)
type source = tok list;
datatype span = Span of command * (source * source * source * source) * bool;
@@ -247,7 +247,9 @@
(tag_stack, active_tag, newline, buffer, present_cont) =
let
val present = fold (fn (tok, flag, 0) =>
- Buffer.add (output_token lex state' tok) #> Buffer.add flag | _ => I);
+ Buffer.add (output_token lex state' tok)
+ #> Buffer.add flag
+ | _ => I);
val Span ((cmd_name, cmd_pos, cmd_tags), srcs, span_newline) = span;
@@ -322,6 +324,10 @@
val tag = (improper -- P.$$$ "%" -- improper) |-- P.!!! (P.tag_name --| improper_end);
+val locale =
+ Scan.option ((P.$$$ "(" -- improper -- P.$$$ "in") |--
+ P.!!! (improper |-- P.xname --| (improper -- P.$$$ ")")));
+
in
fun present_thy lex default_tags is_markup trs src =
@@ -332,10 +338,9 @@
>> (fn d => (NONE, (NoToken, "", d)));
fun markup mark mk flag = Scan.peek (fn d =>
- improper |--
- P.position (Scan.one (T.is_kind T.Command andf is_markup mark o T.val_of)) --
+ improper |-- P.position (Scan.one (T.is_kind T.Command andf is_markup mark o T.val_of)) --
Scan.repeat tag --
- P.!!!! (improper |-- P.position P.text --| improper_end)
+ P.!!!! ((improper -- locale -- improper) |-- P.position P.text --| improper_end)
>> (fn (((tok, pos), tags), txt) =>
let val name = T.val_of tok
in (SOME (name, pos, tags), (mk (name, txt), flag, d)) end));