# HG changeset patch # User wenzelm # Date 1397317614 -7200 # Node ID ae6870efc28dc944a695fc5187907e5c08a6fbc7 # Parent e9bb73d7b6cf6535ca725f85fe295d592af35d23 markup for prose words within formal comments; diff -r e9bb73d7b6cf -r ae6870efc28d src/Pure/PIDE/markup.ML --- a/src/Pure/PIDE/markup.ML Fri Apr 11 23:26:31 2014 +0200 +++ b/src/Pure/PIDE/markup.ML Sat Apr 12 17:46:54 2014 +0200 @@ -62,6 +62,7 @@ val breakN: string val break: int -> T val fbreakN: string val fbreak: T val itemN: string val item: T + val wordsN: string val words: T val hiddenN: string val hidden: T val system_optionN: string val theoryN: string @@ -354,7 +355,9 @@ val (itemN, item) = markup_elem "item"; -(* hidden text *) +(* text properties *) + +val (wordsN, words) = markup_elem "words"; val (hiddenN, hidden) = markup_elem "hidden"; diff -r e9bb73d7b6cf -r ae6870efc28d src/Pure/PIDE/markup.scala --- a/src/Pure/PIDE/markup.scala Fri Apr 11 23:26:31 2014 +0200 +++ b/src/Pure/PIDE/markup.scala Sat Apr 12 17:46:54 2014 +0200 @@ -137,7 +137,9 @@ val SEPARATOR = "separator" - /* hidden text */ + /* text properties */ + + val WORDS = "words" val HIDDEN = "hidden" diff -r e9bb73d7b6cf -r ae6870efc28d src/Pure/Thy/thy_output.ML --- a/src/Pure/Thy/thy_output.ML Fri Apr 11 23:26:31 2014 +0200 +++ b/src/Pure/Thy/thy_output.ML Sat Apr 12 17:46:54 2014 +0200 @@ -24,7 +24,6 @@ val integer: string -> int datatype markup = Markup | MarkupEnv | Verbatim val eval_antiq: Scan.lexicon -> Toplevel.state -> Antiquote.antiq -> string - val eval_antiquote: Scan.lexicon -> Toplevel.state -> Symbol_Pos.text * Position.T -> string val check_text: Symbol_Pos.source -> Toplevel.state -> unit val present_thy: Scan.lexicon -> (string -> string list) -> (markup -> string -> bool) -> (Toplevel.transition * Toplevel.state) list -> Token.T list -> Buffer.T @@ -157,7 +156,7 @@ end; -(* eval_antiquote *) +(* eval_antiq *) fun eval_antiq lex state ((ss, {range = (pos, _), ...}): Antiquote.antiq) = let @@ -169,18 +168,25 @@ val print_modes = space_explode "," (Config.get print_ctxt modes) @ Latex.modes; in Print_Mode.with_modes print_modes (fn () => cmd print_ctxt) () end; + +(* check_text *) + fun eval_antiquote lex state (txt, pos) = let + fun words (Antiquote.Text ss) = [(#1 (Symbol_Pos.range ss), Markup.words)] + | words (Antiquote.Antiq _) = []; + fun expand (Antiquote.Text ss) = Symbol_Pos.content ss | expand (Antiquote.Antiq antiq) = eval_antiq lex state antiq; + val ants = Antiquote.read (Symbol_Pos.explode (txt, pos), pos); + val _ = Position.reports (maps words ants); in if Toplevel.is_toplevel state andalso not (forall Antiquote.is_text ants) then error ("Unknown context -- cannot expand document antiquotations" ^ Position.here pos) else implode (map expand ants) end; - fun check_text {delimited, text, pos} state = (Position.report pos (Markup.language_document delimited); if Toplevel.is_skipped_proof state then () diff -r e9bb73d7b6cf -r ae6870efc28d src/Tools/jEdit/src/rendering.scala --- a/src/Tools/jEdit/src/rendering.scala Fri Apr 11 23:26:31 2014 +0200 +++ b/src/Tools/jEdit/src/rendering.scala Sat Apr 12 17:46:54 2014 +0200 @@ -136,6 +136,8 @@ Markup.CARTOUCHE, Markup.COMMENT, Markup.LANGUAGE, Markup.ML_STRING, Markup.ML_COMMENT) + private val prose_words_elements = Document.Elements(Markup.WORDS) + private val highlight_elements = Document.Elements(Markup.LANGUAGE, Markup.ML_TYPING, Markup.TOKEN_RANGE, Markup.ENTITY, Markup.PATH, Markup.URL, Markup.SORTING, @@ -283,6 +285,12 @@ }).headOption.map(_.info) + /* prose words */ + + def prose_words(range: Text.Range): List[Text.Range] = + snapshot.select(range, Rendering.prose_words_elements, _ => _ => Some(())).map(_.range) + + /* command status overview */ def overview_limit: Int = options.int("jedit_text_overview_limit")