more indentation for quasi_command keywords;
authorwenzelm
Mon Jul 11 10:43:54 2016 +0200 (2016-07-11)
changeset 63434c956d995bec6
parent 63433 aa03b0487bf5
child 63435 7743df69a6b4
more indentation for quasi_command keywords;
src/HOL/Typedef.thy
src/Pure/Pure.thy
src/Tools/jEdit/src/text_structure.scala
     1.1 --- a/src/HOL/Typedef.thy	Mon Jul 11 10:43:27 2016 +0200
     1.2 +++ b/src/HOL/Typedef.thy	Mon Jul 11 10:43:54 2016 +0200
     1.3 @@ -6,7 +6,9 @@
     1.4  
     1.5  theory Typedef
     1.6  imports Set
     1.7 -keywords "typedef" :: thy_goal and "morphisms"
     1.8 +keywords
     1.9 +  "typedef" :: thy_goal and
    1.10 +  "morphisms" :: quasi_command
    1.11  begin
    1.12  
    1.13  locale type_definition =
     2.1 --- a/src/Pure/Pure.thy	Mon Jul 11 10:43:27 2016 +0200
     2.2 +++ b/src/Pure/Pure.thy	Mon Jul 11 10:43:54 2016 +0200
     2.3 @@ -6,13 +6,12 @@
     2.4  
     2.5  theory Pure
     2.6  keywords
     2.7 -    "!!" "!" "+" "--" ":" ";" "<" "<=" "=" "=>" "?" "[" "\<comment>" "\<equiv>"
     2.8 -    "\<leftharpoondown>" "\<rightharpoonup>" "\<rightleftharpoons>"
     2.9 -    "\<subseteq>" "]" "assumes" "attach" "binder" "constrains"
    2.10 -    "defines" "rewrites" "fixes" "for" "if" "in" "includes" "infix"
    2.11 -    "infixl" "infixr" "is" "notes" "obtains" "open" "output"
    2.12 -    "overloaded" "pervasive" "premises" "private" "qualified" "rewrites"
    2.13 -    "shows" "structure" "unchecked" "where" "when" "|"
    2.14 +    "!!" "!" "+" "--" ":" ";" "<" "<=" "=" "=>" "?" "[" "\<comment>" "\<equiv>" "\<leftharpoondown>" "\<rightharpoonup>" "\<rightleftharpoons>"
    2.15 +    "\<subseteq>" "]" "attach" "binder" "for" "if" "in" "infix" "infixl" "infixr" "is"
    2.16 +    "open" "output" "overloaded" "pervasive" "premises" "private" "qualified"
    2.17 +    "structure" "unchecked" "where" "when" "|"
    2.18 +  and "assumes" "constrains" "defines" "fixes" "includes" "notes" "rewrites"
    2.19 +    "obtains" "shows" :: quasi_command
    2.20    and "text" "txt" :: document_body
    2.21    and "text_raw" :: document_raw
    2.22    and "default_sort" :: thy_decl == ""
     3.1 --- a/src/Tools/jEdit/src/text_structure.scala	Mon Jul 11 10:43:27 2016 +0200
     3.2 +++ b/src/Tools/jEdit/src/text_structure.scala	Mon Jul 11 10:43:54 2016 +0200
     3.3 @@ -51,10 +51,20 @@
     3.4            def head_token(line: Int): Option[Token] =
     3.5              nav.iterator(line, 1).toStream.headOption.map(_.info)
     3.6  
     3.7 +          def head_is_quasi_command(line: Int): Boolean =
     3.8 +            head_token(line) match {
     3.9 +              case None => false
    3.10 +              case Some(tok) => keywords.is_quasi_command(tok)
    3.11 +            }
    3.12 +
    3.13            def prev_command: Option[Token] =
    3.14              nav.reverse_iterator(prev_line, 1).
    3.15                collectFirst({ case Text.Info(_, tok) if tok.is_command => tok })
    3.16  
    3.17 +          def prev_span: Iterator[Token] =
    3.18 +            nav.reverse_iterator(prev_line).map(_.info).takeWhile(tok => !tok.is_command)
    3.19 +
    3.20 +
    3.21            def line_indent(line: Int): Int =
    3.22              if (line < 0 || line >= buffer.getLineCount) 0
    3.23              else buffer.getCurrentIndentForLine(line, null)
    3.24 @@ -70,6 +80,10 @@
    3.25              if (keywords.is_command(tok, Keyword.proof_enclose)) indent_size
    3.26              else 0
    3.27  
    3.28 +          def indent_extra: Int =
    3.29 +            if (prev_span.exists(keywords.is_quasi_command(_))) indent_size
    3.30 +            else 0
    3.31 +
    3.32            def indent_structure: Int =
    3.33              nav.reverse_iterator(current_line - 1).scanLeft((0, false))(
    3.34                { case ((ind, _), Text.Info(range, tok)) =>
    3.35 @@ -85,17 +99,25 @@
    3.36  
    3.37            val indent =
    3.38              head_token(current_line) match {
    3.39 -              case None => indent_structure
    3.40 +              case None => indent_structure + indent_extra
    3.41                case Some(tok) =>
    3.42                  if (keywords.is_command(tok, Keyword.theory)) 0
    3.43                  else if (tok.is_command) indent_structure - indent_offset(tok)
    3.44 -                else
    3.45 +                else {
    3.46                    prev_command match {
    3.47 -                    case None => line_indent(prev_line)
    3.48 +                    case None =>
    3.49 +                      val extra =
    3.50 +                        (keywords.is_quasi_command(tok), head_is_quasi_command(prev_line)) match {
    3.51 +                          case (true, true) | (false, false) => 0
    3.52 +                          case (true, false) => - indent_extra
    3.53 +                          case (false, true) => indent_extra
    3.54 +                        }
    3.55 +                      line_indent(prev_line) + extra
    3.56                      case Some(prev_tok) =>
    3.57                        indent_structure - indent_offset(prev_tok) -
    3.58                        indent_indent(prev_tok) + indent_size
    3.59                    }
    3.60 +               }
    3.61              }
    3.62  
    3.63            actions.clear()