# HG changeset patch # User wenzelm # Date 1125934701 -7200 # Node ID 8bf9126d8dcd880694b361d903ec82f309e5f5fc # Parent 63cf42df27231be78d667aedc00374d13e264888 markup commands: optional locale specification; diff -r 63cf42df2723 -r 8bf9126d8dcd src/Pure/Isar/isar_output.ML --- 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));