src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala
changeset 39177 0468964aec11
parent 38853 f593754b0772
child 42327 7c7cc7590eb3
equal deleted inserted replaced
39176:b8fdd3ae8815 39177:0468964aec11
    70                           case None => null
    70                           case None => null
    71                         }
    71                         }
    72                       case _ => null
    72                       case _ => null
    73                     }
    73                     }
    74                 }
    74                 }
    75             } { null }
    75             }
    76           if (markup.hasNext) markup.next.info else null
    76           markup match {
    77 
    77             case Text.Info(_, Some(link)) #:: _ => link
       
    78             case _ => null
       
    79           }
    78         case None => null
    80         case None => null
    79       }
    81       }
    80     }
    82     }
    81   }
    83   }
    82 }
    84 }