markup for prose words within formal comments;
authorwenzelm
Sat Apr 12 17:46:54 2014 +0200 (2014-04-12 ago)
changeset 56548ae6870efc28d
parent 56547 e9bb73d7b6cf
child 56549 7cfc7aa121f3
markup for prose words within formal comments;
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
src/Pure/Thy/thy_output.ML
src/Tools/jEdit/src/rendering.scala
     1.1 --- a/src/Pure/PIDE/markup.ML	Fri Apr 11 23:26:31 2014 +0200
     1.2 +++ b/src/Pure/PIDE/markup.ML	Sat Apr 12 17:46:54 2014 +0200
     1.3 @@ -62,6 +62,7 @@
     1.4    val breakN: string val break: int -> T
     1.5    val fbreakN: string val fbreak: T
     1.6    val itemN: string val item: T
     1.7 +  val wordsN: string val words: T
     1.8    val hiddenN: string val hidden: T
     1.9    val system_optionN: string
    1.10    val theoryN: string
    1.11 @@ -354,7 +355,9 @@
    1.12  val (itemN, item) = markup_elem "item";
    1.13  
    1.14  
    1.15 -(* hidden text *)
    1.16 +(* text properties *)
    1.17 +
    1.18 +val (wordsN, words) = markup_elem "words";
    1.19  
    1.20  val (hiddenN, hidden) = markup_elem "hidden";
    1.21  
     2.1 --- a/src/Pure/PIDE/markup.scala	Fri Apr 11 23:26:31 2014 +0200
     2.2 +++ b/src/Pure/PIDE/markup.scala	Sat Apr 12 17:46:54 2014 +0200
     2.3 @@ -137,7 +137,9 @@
     2.4    val SEPARATOR = "separator"
     2.5  
     2.6  
     2.7 -  /* hidden text */
     2.8 +  /* text properties */
     2.9 +
    2.10 +  val WORDS = "words"
    2.11  
    2.12    val HIDDEN = "hidden"
    2.13  
     3.1 --- a/src/Pure/Thy/thy_output.ML	Fri Apr 11 23:26:31 2014 +0200
     3.2 +++ b/src/Pure/Thy/thy_output.ML	Sat Apr 12 17:46:54 2014 +0200
     3.3 @@ -24,7 +24,6 @@
     3.4    val integer: string -> int
     3.5    datatype markup = Markup | MarkupEnv | Verbatim
     3.6    val eval_antiq: Scan.lexicon -> Toplevel.state -> Antiquote.antiq -> string
     3.7 -  val eval_antiquote: Scan.lexicon -> Toplevel.state -> Symbol_Pos.text * Position.T -> string
     3.8    val check_text: Symbol_Pos.source -> Toplevel.state -> unit
     3.9    val present_thy: Scan.lexicon -> (string -> string list) -> (markup -> string -> bool) ->
    3.10      (Toplevel.transition * Toplevel.state) list -> Token.T list -> Buffer.T
    3.11 @@ -157,7 +156,7 @@
    3.12  end;
    3.13  
    3.14  
    3.15 -(* eval_antiquote *)
    3.16 +(* eval_antiq *)
    3.17  
    3.18  fun eval_antiq lex state ((ss, {range = (pos, _), ...}): Antiquote.antiq) =
    3.19    let
    3.20 @@ -169,18 +168,25 @@
    3.21      val print_modes = space_explode "," (Config.get print_ctxt modes) @ Latex.modes;
    3.22    in Print_Mode.with_modes print_modes (fn () => cmd print_ctxt) () end;
    3.23  
    3.24 +
    3.25 +(* check_text *)
    3.26 +
    3.27  fun eval_antiquote lex state (txt, pos) =
    3.28    let
    3.29 +    fun words (Antiquote.Text ss) = [(#1 (Symbol_Pos.range ss), Markup.words)]
    3.30 +      | words (Antiquote.Antiq _) = [];
    3.31 +
    3.32      fun expand (Antiquote.Text ss) = Symbol_Pos.content ss
    3.33        | expand (Antiquote.Antiq antiq) = eval_antiq lex state antiq;
    3.34 +
    3.35      val ants = Antiquote.read (Symbol_Pos.explode (txt, pos), pos);
    3.36 +    val _ = Position.reports (maps words ants);
    3.37    in
    3.38      if Toplevel.is_toplevel state andalso not (forall Antiquote.is_text ants) then
    3.39        error ("Unknown context -- cannot expand document antiquotations" ^ Position.here pos)
    3.40      else implode (map expand ants)
    3.41    end;
    3.42  
    3.43 -
    3.44  fun check_text {delimited, text, pos} state =
    3.45   (Position.report pos (Markup.language_document delimited);
    3.46    if Toplevel.is_skipped_proof state then ()
     4.1 --- a/src/Tools/jEdit/src/rendering.scala	Fri Apr 11 23:26:31 2014 +0200
     4.2 +++ b/src/Tools/jEdit/src/rendering.scala	Sat Apr 12 17:46:54 2014 +0200
     4.3 @@ -136,6 +136,8 @@
     4.4        Markup.CARTOUCHE, Markup.COMMENT, Markup.LANGUAGE,
     4.5        Markup.ML_STRING, Markup.ML_COMMENT)
     4.6  
     4.7 +  private val prose_words_elements = Document.Elements(Markup.WORDS)
     4.8 +
     4.9    private val highlight_elements =
    4.10      Document.Elements(Markup.LANGUAGE, Markup.ML_TYPING, Markup.TOKEN_RANGE,
    4.11        Markup.ENTITY, Markup.PATH, Markup.URL, Markup.SORTING,
    4.12 @@ -283,6 +285,12 @@
    4.13        }).headOption.map(_.info)
    4.14  
    4.15  
    4.16 +  /* prose words */
    4.17 +
    4.18 +  def prose_words(range: Text.Range): List[Text.Range] =
    4.19 +    snapshot.select(range, Rendering.prose_words_elements, _ => _ => Some(())).map(_.range)
    4.20 +
    4.21 +
    4.22    /* command status overview */
    4.23  
    4.24    def overview_limit: Int = options.int("jedit_text_overview_limit")